Language/OS - Multiplatform Resource Library/LANGUAGE OS.iso/quintus/quintus0.lha/work/rewrite_2.06.2

Text File | 1992-04-03 | 96KB | 2,819 lines

%%%
%%% version 2.00.1
%%%   initial version
%%% version 2.00.2
%%%   fixed rewriting of eqaulity literals
%%% version 2.00.3
%%%   changed "equality_rewriting" to "auto_orient"
%%%   added "outrwr"
%%%   added "outrwt"
%%% version 2.00.4
%%%   fixed priority of rewritten term
%%% version 2.00.5
%%%   added recurive path ordering
%%% version 2.00.6
%%%   added user specified rewrite rules and orderings
%%% version 2.00.7
%%%   moved term rewriting to hypermatching
%%% version 2.00.8
%%%   added lexicographic path ordering
%%% version 2.00.9
%%%   added bound on term rewriting
%%%   moved ground from rewrite to library
%%%   moved unground from rewrite to library
%%%   simplified rewriting of equations
%%%   optimized assert_rewrite_rule
%%%   optimized generate_eq_rewrite_rules
%%% version 2.01.0
%%%   checked clause priority after each hyper-link
%%%   fixed bug in rewrite_clauses which asserted duplicate clauses
%%% version 2.01.1
%%%   modified rewrite_lit so that only arguments of s in not s=t are rewritten
%%% version 2.01.2
%%%   added code to rewrite rewrite rule
%%%   fixed bug in delete_rewrite_rule which sometimes deleted the wrong rule
%%%   modified rewrite_lit so that only arguments of s in s=t are rewritten
%%% version 2.01.3
%%%   moved generation of rewrite rules to hyper-linking
%%%   moved rewriting of input clauses to interpret
%%%   fixed bug when rewriting hyper-links from a unit nucleus
%%%   added code to orient equations
%%%   modified term_order_lpo and term_order_rpo so that order can instantiated
%%%     when calling; that is, let term_order be a test
%%% version 2.01.4
%%%   modified rewriting of equations according to David Plaisted's method
%%%   modified assert_rewrite_rule so that it does not assert a rewrite rule
%%%     if it is an instance of an existing rewrite rule
%%%   fixed method of rewriting rewrite rules so that deleted rewrites rules
%%%     aren't generated again
%%% version 2.01.5
%%%   added code to rewrite asserted clauses
%%%   fixed bug in rewrite_asserted_clauses which caused rewritten clause to
%%%     have clause size and number of non-grounded literals swapped
%%%   fixed bug in rewrite_asserted_clauses which caused duplicate clauses to
%%%     be asserted
%%% version 2.01.8
%%%   modified rewriting of equations so that equations are fully rewritten
%%%   removed use of semi_internal_form from rewrite_asserted_clauses
%%% version 2.01.9
%%%   optimized term rewriting
%%% version 2.02.1
%%%   asserted over_priohm if priority exceeded during term rewriting
%%%   added partial rewrite count
%%%   fixed bug in rewrite_asserted_clauses which caused simplified clauses to
%%%     be printed twice
%%% version 2.02.2
%%%   deleted pulled out form when rewriting asserted clause
%%% version 2.02.6
%%%   optimized lpo_order and rop_order by treating identical terms as
%%%     equivalent
%%% version 2.02.7
%%%   asserted equations corresponding to rewrite rules after simplifying
%%%     rewrite rules
%%% version 2.03.0
%%%   moved rewrite rule simplification to hyper-linking
%%%   set user support flag correctly when asserting equations corresponding to
%%%     rewrite rules
%%%   fixed bug in lexicographical path ordering
%%% version 2.03.2
%%%   modified rewriting of equations so that equations are fully rewritten
%%% version 2.03.4
%%%   modified deleting rewrite rule message
%%%   modified rewrite_clause, rewrite_clause_np, rewrite_lit, rewrite_term,
%%%     and rewrite_term_args_only so that they return immediately if there are
%%%     no rewrite rules
%%% version 2.03.5
%%%   assert equations for rewrite rules only if there are rewrite rules
%%%   removed counters
%%% version 2.03.7
%%%   optimized order_term by saving order of subterms
%%% version 2.04.2
%%%   modified rewriting of equations so that the corresponding rewrite rule
%%%     is not used
%%% version 2.04.3
%%%   erased corresponding equation and pulled out form when simplifying
%%%     rewrite rule
%%% version 2.04.4
%%%   no longer pull out equations at the beginning of rounds
%%%   used restrictive method for rewriting equations
%%%   erased equation associated with rewrite rule only if equation's priority
%%%     exceeded priority bound
%%%   rewrote s fully before attempting to assert a rewrite rule for s=t
%%%   modified rewriting of s=t with s>t to handle case where rewriting s once
%%%     at outer level generates a term smaller than the normal form of t
%%% version 2.04.5
%%%   added restricted_rewrite to control whether restricted or unrestricted
%%%     rewriting of equations is used
%%%   fixed rewrite_asserted_clauses so it erases pulled out forms of rewritten
%%%     clauses
%%%   fixed rewrite_asserted_clauses so it pulls out rewritten input clauses
%%%   generated rewrite rules in rewrite_asserted_clauses
%%% version 2.04.6
%%%   added fixed_priority
%%% version 2.04.7
%%%   when rewriting asserted clauses generate rewrite rules for equation in
%%%     normal form
%%%   added limited rewrite to hyper-linking
%%%   moved code to erase clause corresponding to rewrite rule from
%%%     erase_rewrite_rule to rmrwr_prio
%%% version 2.04.8
%%%   fixed bug in rewrite_outer which prevented priority test from being done
%%% version 2.04.9
%%%   don't assert a rewrite rule if its lhs or rhs has a priority greater
%%%     than the priority bound
%%%   don't assert a clause whose priority is larger than the priority
%%%   sorted clauses by priority before rewriting
%%% version 2.05.2
%%%   fixed assert_rewrite_rule_equations so that it works when neither
%%%     fixed_priority nor slidepriority is specified
%%% version 2.05.3
%%%   added support for quintus prolog
%%%   don't erase rewrite rules corresponding to input equations
%%%   fixed clause rewriting to run when auto_orient and no rewrite rules
%%% version 2.05.4
%%%   don't erase or assert pulled out forms when rewriting clauses
%%%   erase rewrite rules corresponding to input equations
%%%   when rewriting clauses, erase old clause before checking priority of new
%%%     clause
%%%   when rewriting clauses, don't reject new clause if priority bound not set
%%% version 2.05.5
%%%   added equational rewriting
%%%   fixed a couple of bugs which prevented equational rewriting from working
%%%   don't check priority when input clause rewritten
%%%   fixed bug when rewriting input clause
%%% version 2.05.7
%%%   fixed minor equational rewrite bug in rewrite_lit_6
%%% version 2.05.8
%%%   improved the efficiency of order_term_lpo
%%%   don't assert equational rewrite rule if rhs contains variable not
%%%     contained in lhs
%%% version 2.05.9
%%%   fixed bug in lpo term ordering
%%%   added implementation improvement to lpo term ordering
%%%   fixed bug in rewrite_lit
%%%   fixed bug in rewrite_grounded_term_list
%%% version 2.06.0
%%%   fixed print_rewrite so that the used a consistent naming of variables for
%%%     the original and new clause
%%%   fixed bug in rewrite_outer_equational
%%%   fixed assert rewrite rule to print equational rules in both directions
%%%   fixed bug in restricted rewriting
%%%   added early check for unit conflict
%%% version 2.06.1
%%%   added constrained rewriting
%%%   don't print fully rewritten equations and inequation under restricted
%%%     rewriting
%%%   added save_unrestricted_normal_form
%%%   added early unit conflict check to rewrite_rewrite_rules
%%%   rewrite replace rules
%%% version 2.06.2
%%%   added precompute_constraints
%%%   modified rewrite_lit_with_constraints so that restricted rewriting
%%%     doesn't depend on constraints
%%%   modified priority test for non-constrained clause rewriting to check
%%%     priority of rewritten clause rather than rhs of the rewrite rule
%%%   cached lexicographical path ordering
%%%   added index and size bound to cached_rewrite
%%%   added size bound to cached_constraint_consistent
%%%   added size bound to cached_constrained_term_order and
%%%     cached_constrained_term_order_complete
%%%   don't add to constraint when constraint precomputed
%%%   cached constrained subterm rewrites
%%%   removed rpo code as it isn't supported (or used)
%%%   added cache_size
%%%   fixed assert_rewrite_rules_equations/0 to assert equations for equational
%%%     rewrite rules
%%%   added additional time overflow tests
%%%
%%% This is the code for rewriting clauses.  It also contains code for
%%% generating rewrite rules from equations.
%%%

%%%
%%% Rewrite_rule_equations ensures that equations are asserted for each rewrite
%%% rule.
%%%
    rewrite_rule_equations :-
      not(rwr(_,_,_,_)),
      !.
    rewrite_rule_equations :-
      cputime(TT1),
      assert_rewrite_rule_equations,
      cputime(TT2),
      TT3 is TT2 - TT1,
      write_line(5,'Rewrite rule equations(s): ',TT3),
      !.

%%%
%%% Clause_rewriting performs clause rewriting.
%%%
    clause_rewriting :-
      not(auto_orient),
      not(rwr(_,_,_,_)),
      !.
    clause_rewriting :-
      cputime(TT1),
      rewrite_asserted_clauses,
      (rewrite_replace_rules_needed -> (
        abolish(rewrite_replace_rules_needed,0),
        rewrite_replace_rules
      ); true),
      cputime(TT2),
      TT3 is TT2 - TT1,
      write_line(5,'Clause rewriting(s): ',TT3),
      !.

%%%
%%% Rewrite_asserted_clauses rewriting asserted clauses.
%%%
    testit.
    rewrite_asserted_clauses :-
      ((session_no(3),round_no(1)) -> (
        testit
      ); true),
      bagof1(Pr-Cref,{X1,X2,X3,X4,X5,X6,X7,X8,X9a,X9b,X9c,X9d}^
        clause(sent_C(cl(X1,X2,X3,X4,X5,X6,X7,X8,pr(X9a,X9b,X9c,X9d,Pr))),
        true,Cref),Crefs),
      keysort(Crefs,Crefs1),
      abolish(rac_rwr_generated,0),
      rewrite_asserted_clauses_1(Crefs1),
      ((not(prove_result(_)),not(time_overflow)) -> (
        (rac_rwr_generated -> (
          abolish(rac_rwr_generated,0),
          assert_once(rewrite_replace_rules_needed),
          rewrite_rewrite_rules(1),
          ((not(prove_reuslt(_)),not(time_overflow)) -> (
            rewrite_asserted_clauses
          ); true)
        ); true)
      ); true).
    rewrite_asserted_clauses_1([]) :- !.
    rewrite_asserted_clauses_1([_-Cref|Crefs]) :-
      constrained_rewriting,
      restricted_rewrite,
      !,
      clause(sent_C(cl(_,_,by(C,V1,V1,V,_),Input,Sp,Ds,Rep,Dis,_)),true,Cref),
      rewrite_clause_with_constraint(C,Sp,Ds,[],Cts1),
      ((Cts1\==[[C,0,[]]], Cts1\==[[C,1,[]]]) -> (
    print_rewrite_with_constraint(C,Cts1),
        rewrite_asserted_clauses_2(Cts1,Cs1),
        identical_delete_all_duplicates(Cs1,Cs2),
        identical_delete_all(C,Cs2,Cs3),
        (Cs2==Cs3 -> (
          erase(Cref)
        ); true),
        rewrite_asserted_clauses_3(Cs3,Input,Sp,Ds,Rep,Dis)
      ); true),
      abolish(restricted_rewrite,0),
      rewrite_clause_with_constraint(C,Sp,Ds,[],Cts2),
      assert(restricted_rewrite),
      ((Cts2\==[[C,0,[]]], Cts2\==[[C,1,[]]]) -> (
        rewrite_asserted_clauses_2(Cts2,Cs4),
        identical_delete_all_duplicates(Cs4,Cs5),
        identical_delete_all(C,Cs5,Cs6),
        (Cs5\==Cs6 -> (
          generate_rewrite_rule(C,F),
          (F==1 -> (
            assert_once(rac_rwr_generated)
          ); true)
        ); true),
        rewrite_asserted_clauses_4(Cs6,Input,Sp,Ds,Rep,Dis)
      ); (
        generate_rewrite_rule(C,F),
          (F==1 -> (
            assert_once(rac_rwr_generated)
          ); true)
      )),
      ((not(prove_result(_)), not(time_overflow)) -> (
        not(not(rewrite_asserted_clauses_1(Crefs)))
      ); true).
    rewrite_asserted_clauses_1([_-Cref|Crefs]) :-
      restricted_rewrite,
      !,
      clause(sent_C(cl(_,_,by(C1,V1,V1,V,_),Input,Sp,Ds,Rep,Dis,_)),true,Cref),
      rewrite_clause(C1,Sp,Ds,0,C2,F1),
      (C2\==C1 -> (
        erase(Cref),
        (F1==0 -> (
          rewrite_asserted_clauses_5(C2,Input,Sp,Ds,Rep,Dis)
        ); true)
      ); true),
      ((save_unrestricted_normal_form; C1=[_=_]; C1=not(_=_)) -> (
        abolish(restricted_rewrite,0),
        rewrite_clause_np(C1,Sp,Ds,0,C3,F2),
        assert(restricted_rewrite),
        (F2==0 -> (
          generate_rewrite_rule(C3,F3),
          (F3==1 -> (
            assert_once(rac_rwr_generated)
          ); true),
          (save_unrestricted_normal_form -> (
            rewrite_asserted_clauses_5(C3,Input,Sp,Ds,Rep,Dis)
          ); (
            rewrite_asserted_clauses_8(C3)
          ))
        ); true)
      ); true),
      ((not(prove_result(_)), not(time_overflow)) -> (
        not(not(rewrite_asserted_clauses_1(Crefs)))
      ); true).
    rewrite_asserted_clauses_1([_-Cref|Crefs]) :-
      constrained_rewriting,
      !,
      clause(sent_C(cl(_,_,by(C,V1,V1,_,_),Input,Sp,Ds,Rep,Dis,_)),true,Cref),
      rewrite_clause_with_constraint(C,Sp,Ds,[],Cts),
      ((Cts\==[[C,0,[]]], Cts\==[[C,1,[]]]) -> (
        rewrite_asserted_clauses_2(Cts,Cs1),
        identical_delete_all_duplicates(Cs1,Cs2),
        identical_delete_all(C,Cs2,Cs3),
        (Cs2==Cs3 -> (
          erase(Cref)
        ); (
          generate_rewrite_rule(C,F),
          (F==1 -> (
            assert_once(rac_rwr_generated)
          ); true)
        )),
        rewrite_asserted_clauses_4(Cs3,Input,Sp,Ds,Rep,Dis)
      ); true),
      ((not(prove_result(_)), not(time_overflow)) -> (
        not(not(rewrite_asserted_clauses_1(Crefs)))
      ); true).
    rewrite_asserted_clauses_1([_-Cref|Crefs]) :-
      clause(sent_C(cl(_,_,by(C1,V1,V1,_,_),Input,Sp,Ds,Rep,Dis,_)),true,Cref),
      rewrite_clause(C1,Sp,Ds,0,C2,_),
      (C2\==C1 -> (
         erase(Cref),
         rewrite_asserted_clauses_5(C2,Input,Sp,Ds,Rep,Dis)
      ); true),
      generate_rewrite_rule(C2,F),
      (F==1 -> (
        assert_once(rac_rwr_generated)
      ); true),
      ((not(prove_result(_)), not(time_overflow)) -> (
        not(not(rewrite_asserted_clauses_1(Crefs)))
      ); true).
    rewrite_asserted_clauses_2([],[]) :- !.
    rewrite_asserted_clauses_2([[C,_,_]|Cts],[C|Cs]) :-
      rewrite_asserted_clauses_2(Cts,Cs).
    rewrite_asserted_clauses_3([],_,_,_,_,_) :- !.
    rewrite_asserted_clauses_3([C|Cs],Input,Sp,Ds,Rep,Dis) :-
      rewrite_asserted_clauses_5(C,Input,Sp,Ds,Rep,Dis),
      rewrite_asserted_clauses_3(Cs,Input,Sp,Ds,Rep,Dis).
    rewrite_asserted_clauses_4([],_,_,_,_,_) :- !.
    rewrite_asserted_clauses_4([C|Cs],Input,Sp,Ds,Rep,Dis) :-
      generate_rewrite_rule(C,F),
      (F==1 -> (
        assert_once(rac_rwr_generated)
      ); true),
      ((restricted_rewrite, save_unrestricted_normal_form) -> (
        rewrite_asserted_clauses_5(C,Input,Sp,Ds,Rep,Dis)
      ); true),
      rewrite_asserted_clauses_4(Cs,Input,Sp,Ds,Rep,Dis).
    rewrite_asserted_clauses_5(C,Input,Sp,Ds,Rep,Dis) :-
      calculate_priority_clause(C,Sp,Ds,Pr),
      rewrite_asserted_clauses_6(C,Sp,Ds,Pr,Input),
      rewrite_asserted_clauses_7(C,Input,Sp,Ds,Rep,Dis,Pr),
      !.
    rewrite_asserted_clauses_5(_,_,_,_,_,_).
    rewrite_asserted_clauses_6(C2,Sp,Ds,Pr,0) :-
      priority_bound(PrioBound),
      !,
      check_prioritybound(Pr,PrioBound),
      !.
    rewrite_asserted_clauses_6(_,_,_,_,_).
    rewrite_asserted_clauses_7(C2,Input,Sp,Ds,Rep,Dis,Pr) :-
      delete_all_instances,
      !,
      vars_tail(C2,V),
      not(instance_clause_C(C2,V)),
      rewrite_asserted_clauses_8(C2),
      linearize_term(C2,C,V1,V2),
      clause_size(C2,CSize),
      vars_literals(C2,W),
      compute_V_lits(W,0,NLits),
      assertz(sent_C(cl(CSize,NLits,by(C,V1,V2,V,W),Input,Sp,Ds,Rep,Dis,Pr))),
      !.
    rewrite_asserted_clauses_7(C2,Input,Sp,Ds,Rep,Dis,Pr) :-
      linearize_term(C2,C,V1,V2),
      vars_tail(C2,V),
      clause_size(C2,CSize),
      not(duplicate_clause_C(CSize,C2,V)),
      rewrite_asserted_clauses_8(C2),
      vars_literals(C2,W),
      compute_V_lits(W,0,NLits),
      assertz(sent_C(cl(CSize,NLits,by(C,V1,V2,V,W),Input,Sp,Ds,Rep,Dis,Pr))),
      !.
    rewrite_asserted_clauses_8([U]) :-
      check_unit_conflict_C(U),
      !,
      assert_tryresult('unsatisfiable'),
      assert_prooftype('UC').
    rewrite_asserted_clauses_8(_).

%%%
%%% Rewrite_clause rewrites a clause.
%%%
    rewrite_clause(C,_,_,_,C,0) :-
      not(rwr(_,_,_,_)),
      !.
    rewrite_clause(C1,Sp,Ds,0,C2,F) :-
      term_size(C1,Size),
      vars_tail(C1,V),
      (restricted_rewrite -> (
        ((cached_restricted_clause_rewrite(Size,C1,var(V1,V2,V3),C2),
            not(not(const_list(V))),
            not(not(const_list(V3))),
            not(not((V1=V2,const_list(V))))) -> (
          assert(clause_rewrite_found)
        ); true)
      ); (
        ((cached_nonrestricted_clause_rewrite(Size,C1,var(V1,V2,V3),C2),
            not(not(const_list(V))),
            not(not(const_list(V3))),
            not(not((V1=V2,const_list(V))))) -> (
          assert(clause_rewrite_found)
        ); true)
      )),
      (clause_rewrite_found -> (
        abolish(clause_rewrite_found,0)
      ); (
        (var(Sp) -> (
          Sp1=sp(0,0,0),
          Ds1=ds(0,0,0)
        ); (
          Sp1=Sp,
          Ds1=Ds
        )),
        calculate_priority_clause(C1,Sp1,Ds1,pr(_,_,_,_,Pr)),
        assert(saved_clause_size(Pr)),
        rewrite_clause_1(C1,Sp1,Ds1,0,C2,F),
        abolish(saved_clause_size,1),
        counter(cached_clause_rewrite_count,N),
        cache_size(CacheSize),
        (N > CacheSize -> (
          write_line(0,'*** cleared cached_clause_rewrite: ',N),
          set_counter(cached_clause_rewrite_count,0),
          abolish(cached_restricted_clause_rewrite,4),
          abolish(cached_nonrestricted_clause_rewrite,4)
        ); true),
        increment_counter(cached_clause_rewrite_count,Size),
        linearize_term(C1,C3,V4,V5),
        (restricted_rewrite -> (
          assert(cached_restricted_clause_rewrite(Size,C3,var(V4,V5,V),C2))
        ); (
          assert(cached_nonrestricted_clause_rewrite(Size,C3,var(V4,V5,V),C2))
        )),
        print_rewrite(C1,C2)
      )).
    rewrite_clause(C1,_,_,1,C2,F) :-
      rewrite_clause_1(C1,_,_,1,C2,F),
      print_rewrite(C1,C2).
    rewrite_clause_1([],_,_,_,[],0) :- !.
    rewrite_clause_1([L1|Ls1],Sp,Ds,Lim,[L2|Ls2],F) :-
      rewrite_lit(L1,Sp,Ds,Lim,L2,F1),
      rewrite_clause_2(Ls1,Sp,Ds,Lim,Ls2,F,F1).
    rewrite_clause_2(Ls1,Sp,Ds,Lim,Ls2,F,0) :-
      rewrite_clause_1(Ls1,Sp,Ds,Lim,Ls2,F).
    rewrite_clause_2(Ls1,Sp,Ds,Lim,Ls2,1,1) :-
      rewrite_clause_1(Ls1,Sp,Ds,Lim,Ls2,_).

%%%
%%% Rewrite_clause_np rewrites a clause without printing the rewrite even if
%%% outrwt is asserted.
%%%
    rewrite_clause_np(C1,Sp,Ds,Lim,C2,F) :-
      (outrwt -> (
        abolish(outrwt,0),
        rewrite_clause(C1,Sp,Ds,Lim,C2,F),
        assert(outrwt)
      ); (
        rewrite_clause(C1,Sp,Ds,Lim,C2,F)
      )),
      !.

%%%
%%% Rewrite_lit rewrites a literal.
%%%
    rewrite_lit(S=T,Sp,Ds,Lim,L,F) :-
      restricted_rewrite,
      !,
      order_term(S,O,T),
      rewrite_lit_2(S,O,T,Sp,Ds,Lim,L,F),
      !.
    rewrite_lit(S=T,Sp,Ds,Lim,L,F) :-
      !,
      remove_rewrite_rule(S=T),
      rewrite_term(S,Sp,Ds,Lim,S1,F1),
      restore_rewrite_rule(S=T),
      remove_rewrite_rule(T=S),
      rewrite_term(T,Sp,Ds,Lim,T1,F2),
      restore_rewrite_rule(T=S),
      orient_equation(S1=T1,L),
      rewrite_lit_1(F1,F2,F),
      !.
    rewrite_lit(not S1=T1,Sp,Ds,Lim,not S2=T2,F) :-
      restricted_rewrite,
      !,
      rewrite_term_args_only(S1,Sp,Ds,Lim,S2,F1),
      rewrite_term(T1,Sp,Ds,Lim,T2,F2),
      rewrite_lit_1(F1,F2,F),
      !.
    rewrite_lit(not L1,Sp,Ds,Lim,not L2,F) :-
      rewrite_term(L1,Sp,Ds,Lim,L2,F),
      !.
    rewrite_lit(L1,Sp,Ds,Lim,L2,F) :-
      rewrite_term(L1,Sp,Ds,Lim,L2,F),
      !.
    rewrite_lit_1(1,_,1) :- !.
    rewrite_lit_1(_,1,1) :- !.
    rewrite_lit_1(_,_,0) :- !.
    rewrite_lit_2(S,>,T,Sp,Ds,Lim,L,F) :-
      !,
      rewrite_term(T,Sp,Ds,Lim,T1,F1),
      rewrite_lit_4(S,Sp,Ds,Lim,T1,L,F1,F),
      !.
    rewrite_lit_2(S,<,T,Sp,Ds,Lim,L,F) :-
      !,
      rewrite_term(S,Sp,Ds,Lim,S1,F1),
      rewrite_lit_4(T,Sp,Ds,Lim,S1,L,F1,F),
      !.
    rewrite_lit_2(S1,_,T1,Sp,Ds,Lim,S2=T2,F) :-
      rewrite_term(S1,Sp,Ds,Lim,S2,F1),
      rewrite_term(T1,Sp,Ds,Lim,T2,F2),
      rewrite_lit_1(F1,F2,F),
      !.
    rewrite_lit_3(S1,S2,T2,_,_,_,S2=T2,0) :-
      S1==S2,
      !.
    rewrite_lit_3(_,S2,T2,Sp,Ds,Lim,L,F) :-
      rewrite_term(S2,Sp,Ds,Lim,S3,F),
      orient_equation(S3=T2,L),
      !.
    rewrite_lit_4(S1,Sp,Ds,Lim,T2,T2=S3,F1,F) :-
      vars_tail(S1,V),
      rewrite_lit_5(Lim,S1,S2,V),
      order_term(S2,<,T2),
      !,
      rewrite_term(S2,Sp,Ds,Lim,S3,F2),
      rewrite_lit_1(F1,F2,F),
      !.
    rewrite_lit_4(S1,Sp,Ds,Lim,T2,L,F1,F) :-
      rewrite_term_args_only(S1,Sp,Ds,Lim,S2,F2),
      rewrite_lit_3(S1,S2,T2,Sp,Ds,Lim,L,F3),
      rewrite_lit_1(F1,F2,F4),
      rewrite_lit_1(F4,F3,F),
      !.
    rewrite_lit_5(0,S1,S2,V) :-
      rwr((S1->S2),var(V1,V2,_),_,_),
      unify_lists(V1,V2),
      not(not(const_list(V))).
    rewrite_lit_5(0,S1,S2,V) :-
      equational_rewrite,
      rwr((S1=S2),var(V1,V2,_),_,_),
      unify_lists(V1,V2),
      not(not(const_list(V))),
      order_term(S1,>,S2).
    rewrite_lit_5(1,S1,S2,V) :-
      rwr((S1->S2),var(V1,V2,_),0,_),
      unify_lists(V1,V2),
      not(not(const_list(V))).

%%%
%%% Rewrite_term_args_only rewrites the arguments of a term.
%%%
    rewrite_term_args_only(T1,Sp,Ds,Lim,T2,F1) :-
      ground(T1,T3,Vs,Cs),
      functor(T3,F,N),
      rewrite_grounded_arguments(N,T3,Sp,Ds,Vs,Cs,Lim,As2,F1),
      T4=..[F|As2],
      unground(T4,T2,Vs,Cs),
      !.

%%%
%%% Rewrite_grounded_arguments rewrites the arguments of a grounded term.
%%%
    rewrite_grounded_arguments(0,_,_,_,_,_,_,[],0) :- !.
    rewrite_grounded_arguments(N,T,Sp,Ds,Vs,Cs,0,[T2|Ts2],F1) :-
      equational_rewrite,
      !,
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,T1),
      rewrite_term_1(T1,Sp,Ds,Vs,Cs,0,T3,F2),
      rewrite_term_5(T3,Sp,Ds,Vs,Cs,0,T4,F2,F3),
      rewrite_term_9(T3,T4,Sp,Ds,Vs,Cs,0,T2,F3,F),
      N3 is N-1,
      rewrite_grounded_arguments_1(N3,T,Sp,Ds,Vs,Cs,0,F,Ts2,F1),
      !.
    rewrite_grounded_arguments(N,T,Sp,Ds,Vs,Cs,Lim,[T2|Ts2],F1) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,T1),
      rewrite_term_1(T1,Sp,Ds,Vs,Cs,Lim,T2,F),
      N3 is N-1,
      rewrite_grounded_arguments_1(N3,T,Sp,Ds,Vs,Cs,Lim,F,Ts2,F1),
      !.
    rewrite_grounded_arguments_1(0,_,_,_,_,_,_,1,[],1) :- !.
    rewrite_grounded_arguments_1(N,T,_,_,_,_,_,1,[Ti|Ts],1) :-
      !,
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,Ti),
      N3 is N-1,
      rewrite_grounded_arguments_1(N3,T,_,_,_,_,_,1,Ts,1).
    rewrite_grounded_arguments_1(N,T,Sp,Ds,Vs,Cs,Lim,_,Ts2,F) :-
      !,
      rewrite_grounded_arguments(N,T,Sp,Ds,Vs,Cs,Lim,Ts2,F).

%%%
%%% Rewrite_term reduces a term to its normal form.
%%%
    rewrite_term(T1,Sp,Ds,0,T2,F) :-
      equational_rewrite,
      !,
      ground(T1,T3,Vs,Cs),
      rewrite_term_1(T3,Sp,Ds,Vs,Cs,0,T4,F1),
      rewrite_term_5(T4,Sp,Ds,Vs,Cs,0,T5,F1,F2),
      rewrite_term_9(T4,T5,Sp,Ds,Vs,Cs,0,T6,F2,F),
      unground(T6,T2,Vs,Cs),
      !.
    rewrite_term(T1,Sp,Ds,Lim,T2,F) :-
      ground(T1,T3,Vs,Cs),
      rewrite_term_1(T3,Sp,Ds,Vs,Cs,Lim,T4,F),
      unground(T4,T2,Vs,Cs),
      !.
    rewrite_term_1(T1,Sp,Ds,Vs,Cs,Lim,T2,F1) :-
      rewrite_outer(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      rewrite_term_2(T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_2(T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_2(T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_args(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_3(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_3(_,T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_3(T1,T2,_,_,_,_,_,_,T2,0) :-
      T1==T2,
      !.
    rewrite_term_3(_,T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_outer(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_4(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_4(_,T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_4(T1,T2,_,_,_,_,_,_,T2,0) :-
      T1==T2,
      !.
    rewrite_term_4(_,T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_args(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_3(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_5(T,_,_,_,_,_,T,1,1) :- !.
    rewrite_term_5(T1,Sp,Ds,Vs,Cs,Lim,T2,0,F1) :-
      rewrite_outer_equational(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      rewrite_term_6(T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_6(T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_6(T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_args_equational(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_7(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_7(_,T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_7(T1,T2,_,_,_,_,_,_,T2,0) :-
      T1==T2,
      !.
    rewrite_term_7(_,T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_outer_equational(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_8(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_8(_,T,_,_,_,_,_,1,T,1) :- !.
    rewrite_term_8(T1,T2,_,_,_,_,_,_,T2,0) :-
      T1==T2,
      !.
    rewrite_term_8(_,T1,Sp,Ds,Vs,Cs,Lim,_,T2,F1) :-
      rewrite_args_equational(T1,Sp,Ds,Vs,Cs,Lim,T3,F),
      !,
      rewrite_term_7(T1,T3,Sp,Ds,Vs,Cs,Lim,F,T2,F1),
      !.
    rewrite_term_9(_,T,_,_,_,_,_,T,1,1) :- !.
    rewrite_term_9(T1,T2,_,_,_,_,_,T2,_,0) :-
      T1==T2,
      !.
    rewrite_term_9(_,T1,Sp,Ds,Vs,Cs,Lim,T2,_,F) :-
      rewrite_term_1(T1,Sp,Ds,Vs,Cs,Lim,T3,F1),
      rewrite_term_10(T1,T3,Sp,Ds,Vs,Cs,Lim,T2,F1,F),
      !.
    rewrite_term_10(_,T,_,_,_,_,_,T,1,1) :- !.
    rewrite_term_10(T1,T2,_,_,_,_,_,T2,_,0) :-
      T1==T2,
      !.
    rewrite_term_10(_,T1,Sp,Ds,Vs,Cs,Lim,T2,_,F) :-
      rewrite_term_5(T1,Sp,Ds,Vs,Cs,Lim,T3,0,F1),
      rewrite_term_9(T1,T3,Sp,Ds,Vs,Cs,Lim,T2,F1,F),
      !.

%%%
%%% Rewrite_outer fully reduces a term at the outer most level.
%%%
    rewrite_outer(T1,_,_,_,_,Lim,T2,0) :-
      not(fixed_priority),
      not(slidepriority),
      !,
      rewrite_outer_1(T1,T2,Lim).
    rewrite_outer(T1,Sp,Ds,Vs,Cs,0,T2,F1) :-
      rewrite_outer_2(T1,Sp,Ds,Vs,Cs,T2,F1),
      !.
    rewrite_outer(T1,_,_,_,_,1,T2,0) :-
      rewrite_outer_1(T1,T2,1),
      !.
    rewrite_outer_1(T1,T2,0) :-
      rwr((T1->T3),var(V1,V1,_),_,_),
      const_list(V),
      not(dont_use_rewrite_rule_outer(T1=T3,V)),
      !,
      rewrite_outer_1(T3,T2,0).
    rewrite_outer_1(T1,T2,1) :-
      rwr((T1->T3),var(V1,V1,_),0,_),
      const_list(V),
      not(dont_use_rewrite_rule_outer(T1=T3,V)),
      !,
      rewrite_outer_1(T3,T2,1).
    rewrite_outer_1(T,T,_).
    rewrite_outer_2(T1,Sp,Ds,Vs,Cs,T2,F1) :-
      rwr((T1->T3),var(V1,V1,_),_,_),
      const_list(V),
      not(dont_use_rewrite_rule_outer(T1=T3,V)),
      !,
      rewrite_outer_3(T1,T3,Sp,Ds,Vs,Cs,T2,F1).
    rewrite_outer_2(T,_,_,_,_,T,0).
    rewrite_outer_3(T1,T2,Sp,Ds,Vs,Cs,T2,1) :-
      nonvar(Sp),
      priority_bound(PrioBound),
      unground(T1,T3,Vs,Cs),
      unground(T2,T4,Vs,Cs),
      calculate_priority_clause([T3],Sp,Ds,pr(_,_,_,_,Pr1)),
      calculate_priority_clause([T4],Sp,Ds,pr(_,_,_,_,Pr2)),
      (retract(saved_clause_size(Pr3)) -> (
        Pr is Pr3 - Pr1 + Pr2,
        assert(saved_clause_size(Pr))
      ); (
        Pr is  Pr2
      )),
      not(check_prioritybound(pr(_,_,_,_,Pr),PrioBound)),
      !.
    rewrite_outer_3(_,T3,Sp,Ds,Vs,Cs,T2,F1) :-
      !,
      rewrite_outer_2(T3,Sp,Ds,Vs,Cs,T2,F1).

%%%
%%% Rewrite_outer_equational fully reduces a term at the outer most level using
%%% equational rewrite rules.
%%%
    rewrite_outer_equational(T,_,_,_,_,_,T,0) :-
      not(equational_rewrite),
      !.
    rewrite_outer_equational(T1,_,_,Vs,Cs,Lim,T2,0) :-
      not(fixed_priority),
      not(slidepriority),
      !,
      rewrite_outer_equational_1(T1,T2,Vs,Cs,Lim).
    rewrite_outer_equational(T1,Sp,Ds,Vs,Cs,0,T2,F1) :-
      rewrite_outer_equational_2(T1,Sp,Ds,Vs,Cs,T2,F1),
      !.
    rewrite_outer_equational(T1,_,_,Vs,Cs,1,T2,0) :-
      rewrite_outer_equational_1(T1,T2,Vs,Cs,1),
      !.
    rewrite_outer_equational_1(T1,T2,Vs,Cs,0) :-
      rwr(T1=T3,var(V1,V1,_),_,_),
      unground({T1,T3},{T4,T5},Vs,Cs),
      order_term(T4,>,T5),
      !,
      rewrite_outer_equational_1(T3,T2,Vs,Cs,0).
    rewrite_outer_equational_1(T1,T2,Vs,Cs,1) :-
      rwr(T1=T3,var(V1,V1,_),0,_),
      unground({T1,T3},{T4,T5},Vs,Cs),
      order_term(T4,>,T5),
      !,
      rewrite_outer_equational_1(T3,T2,Vs,Cs,1).
    rewrite_outer_equational_1(T,T,_,_,_).
    rewrite_outer_equational_2(T1,Sp,Ds,Vs,Cs,T2,F1) :-
      rwr(T1=T3,var(V1,V1,_),_,_),
      unground({T1,T3},{T4,T5},Vs,Cs),
      order_term(T4,>,T5),
      !,
      rewrite_outer_equational_3(T1,T3,T5,Sp,Ds,Vs,Cs,T2,F1).
    rewrite_outer_equational_2(T,_,_,_,_,T,0).
    rewrite_outer_equational_3(T1,T2,T3,Sp,Ds,_,_,T2,1) :-
      nonvar(Sp),
      priority_bound(PrioBound),
      calculate_priority_clause([T1],Sp,Ds,pr(_,_,_,_,Pr1)),
      calculate_priority_clause([T3],Sp,Ds,pr(_,_,_,_,Pr2)),
      (retract(saved_clause_size(Pr3)) -> (
        Pr is Pr3 - Pr1 + Pr2,
        assert(saved_clause_size(Pr))
      ); (
        Pr is Pr2
      )),
      not(check_prioritybound(pr(_,_,_,_,Pr),PrioBound)),
      !.
    rewrite_outer_equational_3(_,T3,_,Sp,Ds,Vs,Cs,T2,F1) :-
      !,
      rewrite_outer_equational_2(T3,Sp,Ds,Vs,Cs,T2,F1).

%%%
%%% Rewrite_args fully reduces the arguments of a term.
%%%
    rewrite_args(T1,Sp,Ds,Vs,Cs,Lim,T2,F1) :-
      functor(T1,F,N),
      rewrite_args_1(N,T1,Sp,Ds,Vs,Cs,Lim,As,F1),
      T2=..[F|As],
      !.
    rewrite_args_1(0,_,_,_,_,_,_,[],0) :- !.
    rewrite_args_1(N,T,Sp,Ds,Vs,Cs,Lim,[A|As],F1) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,A1),
      rewrite_term_1(A1,Sp,Ds,Vs,Cs,Lim,A,F),
      N3 is N-1,
      rewrite_args_2(N3,T,Sp,Ds,Vs,Cs,Lim,F,As,F1),
      !.
    rewrite_args_2(0,_,_,_,_,_,_,1,[],1) :- !.
    rewrite_args_2(N,T,_,_,_,_,Lim,1,[A|As],F) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,A),
      N3 is N-1,
      !,
      rewrite_args_2(N3,T,_,_,_,_,Lim,1,As,F).
    rewrite_args_2(N,T,Sp,Ds,Vs,Cs,Lim,_,As,F) :-
      !,
      rewrite_args_1(N,T,Sp,Ds,Vs,Cs,Lim,As,F).

%%%
%%% Rewrite_args_equational fully reduces the arguments of a term using
%%% equational rewrite rules.
%%%
    rewrite_args_equational(T,_,_,_,_,_,T,0) :-
      not(equational_rewrite),
      !.
    rewrite_args_equational(T1,Sp,Ds,Vs,Cs,Lim,T2,F1) :-
      functor(T1,F,N),
      rewrite_args_equational_1(N,T1,Sp,Ds,Vs,Cs,Lim,As,F1),
      T2=..[F|As],
      !.
    rewrite_args_equational_1(0,_,_,_,_,_,_,[],0) :- !.
    rewrite_args_equational_1(N,T,Sp,Ds,Vs,Cs,Lim,[A|As],F1) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,A1),
      rewrite_term_5(A1,Sp,Ds,Vs,Cs,Lim,A,0,F),
      N3 is N-1,
      rewrite_args_equational_2(N3,T,Sp,Ds,Vs,Cs,Lim,F,As,F1),
      !.
    rewrite_args_equational_2(0,_,_,_,_,_,_,1,[],1) :- !.
    rewrite_args_equational_2(N,T,_,_,_,_,Lim,1,[A|As],F) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,A),
      N3 is N-1,
      !,
      rewrite_args_equational_2(N3,T,_,_,_,_,Lim,1,As,F).
    rewrite_args_equational_2(N,T,Sp,Ds,Vs,Cs,Lim,_,As,F) :-
      !,
      rewrite_args_equational_1(N,T,Sp,Ds,Vs,Cs,Lim,As,F).

%%%
%%% Print_rewrite prints a rewritten term.
%%%
    print_rewrite(_,_) :-
      not(outrwt),
      !.
    print_rewrite(C1,C2) :-
      C1==C2,
      !.
    print_rewrite(C1,C2) :-
      write_line(10,'rewriting:'),
      not(not(print_rewrite_1(C1,C2))),
      !.
    print_rewrite_1(C1,C2) :-
      vars_tail(C1,V),
      var_list(V),
      write_line(13,'orig: ',C1),
      write_line(13,'new:  ',C2),
      !.

%%%
%%% Rewrite_rewrite_rules rewrites all non-user rewrite rules.
%%%
    rewrite_rewrite_rules(0).
    rewrite_rewrite_rules(1) :-
      bagof1(rwr(R,V,F,0),rwr(R,V,F,0),Rs),
      rewrite_rewrite_rules_1(Rs,Fs),
      ((prove_result(_);time_overflow) -> true; (
        or_list(Fs,F),
        rewrite_rewrite_rules(F)
      )).
    rewrite_rewrite_rules_1([],[]) :- !.
    rewrite_rewrite_rules_1([rwr(R,V,F,U)|Rs],[0|Fs]) :-
      rewrite_rule_ref(rwr(R,V,F,U),Ref),
      instance_rewrite_rule_ref(Ref),
      !,
      erase_rewrite_rule(rwr(R,V,F,U)),
      rewrite_rewrite_rules_1(Rs,Fs).
    rewrite_rewrite_rules_1([rwr(R,var(V1,V1,V),F1,U)|Rs],[F2|Fs]) :-
      constrained_rewriting,
      !,
      arg(1,R,S),
      arg(2,R,T),
      ((restricted_rewrite ->
        abolish(restricted_rewrite,0),
        rewrite_clause_with_constraint([S=T],_,_,[],Cts1),
        assert(restricted_rewrite)
      ); (
        rewrite_clause_with_constraint([S=T],_,_,[],Cts1)
      )),
      rewrite_rewrite_rules_2(Cts1,S=T,Cts2),
      (Cts1\==Cts2 -> (
        Cts3=Cts2
      ); (
        erase_rewrite_rule(rwr(R,var(V1,V1,V),F1,U)),
        (restricted_rewrite -> (
          abolish(restricted_rewrite,0),
          rewrite_clause_with_constraint([S=T],_,_,[],Cts3),
          assert(restricted_rewrite)
        ); (
          rewrite_clause_with_constraint([S=T],_,_,[],Cts3)
        ))
      )),
      rewrite_rewrite_rules_3(Cts3,Fs1),
      or_list(Fs1,F2),
      ((prove_result(_);time_overflow) -> (
        Fs=[]
      ); (
        rewrite_rewrite_rules_1(Rs,Fs)
      )).
    rewrite_rewrite_rules_1([rwr(R,var(V1,V1,V),F1,U)|Rs],[F2|Fs]) :-
      arg(1,R,S),
      arg(2,R,T),
      (restricted_rewrite -> (
        abolish(restricted_rewrite,0),
        remove_rewrite_rule(S=T),
        rewrite_term(S,_,_,0,S1,_),
        restore_rewrite_rule(S=T),
        remove_rewrite_rule(T=S),
        rewrite_term(T,_,_,0,T1,_),
        restore_rewrite_rule(T=S),
        assert(restricted_rewrite)
      ); (
        remove_rewrite_rule(S=T),
        rewrite_term(S,_,_,0,S1,_),
        restore_rewrite_rule(S=T),
        remove_rewrite_rule(T=S),
        rewrite_term(T,_,_,0,T1,_),
        restore_rewrite_rule(T=S)
      )),
      ((S\==S1; T\==T1) -> (
        erase_rewrite_rule(rwr(R,var(V1,V1,V),F1,U)),
        generate_rewrite_rule([S1=T1],F2),
        ((F2==1, check_unit_conflict_C(S1=T1)) -> (
          Fs=[],
          assert_tryresult('unsatisfiable'),
          assert_prooftype('UC')
          ); (
            rewrite_rewrite_rules_1(Rs,Fs)
        ))
      ); (
        F2=0,
        rewrite_rewrite_rules_1(Rs,Fs)
      )).
    rewrite_rewrite_rules_2([],_,[]) :- !.
    rewrite_rewrite_rules_2([[[S1=T1],_,_]|Cts1],S=T,Cts2) :-
      (S1=T1)==(S=T),
      !,
      rewrite_rewrite_rules_2(Cts1,S=T,Cts2).
    rewrite_rewrite_rules_2([Ct|Cts1],S=T,[Ct|Cts2]) :-
      rewrite_rewrite_rules_2(Cts1,S=T,Cts2).
    rewrite_rewrite_rules_3([],[]) :- !.
    rewrite_rewrite_rules_3([[[S=T],_,_]|Cts],[F|Fs]) :-
      generate_rewrite_rule([S=T],F),
      (F==1 -> (
        (check_unit_conflict_C(S=T) -> (
          Fs=[],
          assert_tryresult('unsatisfiable'),
          assert_prooftype('UC')
        ); (
          rewrite_rewrite_rules_4(Cts,[],Cts1),
          rewrite_rewrite_rules_3(Cts1,Fs)
        ))
      ); (
        rewrite_rewrite_rules_3(Cts,Fs)
      )).
    rewrite_rewrite_rules_4([],Cts,Cts) :- !.
    rewrite_rewrite_rules_4([[[S=T],0,Con]|Cts1],Cts2,Cts3) :-
      !,
      (restricted_rewrite -> (
        abolish(restricted_rewrite,0),
        rewrite_clause_with_constraint([S=T],_,_,Con,Cts4),
        assert(restricted_rewrite)
      ); (
        rewrite_clause_with_constraint([S=T],_,_,Con,Cts4)
      )),
      append(Cts2,Cts4,Cts5),
      rewrite_rewrite_rules_4(Cts1,Cts5,Cts3).
    rewrite_rewrite_rules_4([Ct|Cts1],Cts2,Cts3) :-
      append(Cts2,[Ct],Cts4),
      rewrite_rewrite_rules_4(Cts1,Cts4,Cts3).

%%%
%%% Erase_rewrite_rule erases a rewrite rule.
%%%
    erase_rewrite_rule(rwr(R,V,F,U)) :-
      abolish_rewrite_caches,
      not(not(erase_rewrite_rule_1(rwr(R,V,F,U)))),
      not(not(eras  rewrite_rule_2(R,V))),
      !.
    erase_rewrite_rule(_).
    erase_rewrite_rule_1(rwr(R,var(V1,V1,V),F,U)) :-
      const_list(V),
      retract(rwr(R,var(V1,V1,V),F,U)),
      !.
    erase_rewrite_rule_2(R,var(V1,V1,V)) :-
      outrwr,
      !,
      arg(1,R,S),
      arg(2,R,T),
      var_list(V),
      write_line(10,'deleting rewrite rule: ',S,'->',T),
      !.
    erase_rewrite_rule_2(_,_).

%%%
%%% Generate_rewrite_rule generates a rewrite rule from an equation.
%%%
    generate_rewrite_rule(_,0) :-
      not(auto_orient),
      !.
    generate_rewrite_rule([S=T],0) :-
      S==T,
      !.
    generate_rewrite_rule([S=T],F) :-
      !,
      order_term(S,O,T),
      generate_rewrite_rule_1(S,O,T,F).
    generate_rewrite_rule(_,0).
    generate_rewrite_rule_1(S,>,T,F) :-
      !,
      assert_rewrite_rule(0,(S->T),F).
    generate_rewrite_rule_1(S,<,T,F) :-
      !,
      assert_rewrite_rule(0,(T->S),F).
    generate_rewrite_rule_1(S,_,T,F) :-
      equational_rewrite,
      !,
      assert_rewrite_rule(0,(S=T),F).
    generate_rewrite_rule_1(_,_,_,0).

%%%
%%% Assert_rewrite_rule asserts a rewrite rule into the database.
%%%
    assert_rewrite_rule(_,R,0) :-
      arg(1,R,S),
      priority_bound(PrioBound),
      calculate_priority_clause([S],sp(0,0,0),ds(0,0,0),pr(_,_,_,_,Pr)),
      Pr > PrioBound,
      !,
      assert_once(over_priohm).
    assert_rewrite_rule(_,R,0) :-
      arg(2,R,T),
      priority_bound(PrioBound),
      calculate_priority_clause([T],sp(0,0,0),ds(0,0,0),pr(_,_,_,_,Pr)),
      Pr > PrioBound,
      !,
      assert_once(over_priohm).
    assert_rewrite_rule(U,(S->T),1) :-
      vars_tail((S->T),V),
      not(instance_rewrite_rule((S->T),V)),
      !,
      assert_rewrite_rule_1((S->T),F),
      abolish_rewrite_caches,
      linearize_term((S->T),(S1->T1),V1,V2),
      assertz(rwr((S1->T1),var(V1,V2,V),F,U)),
      print_rewrite_rule(rwr((S1->T1),var(V1,V2,V),F,U)),
      !.
    assert_rewrite_rule(U,(S->T),0) :- !.
    assert_rewrite_rule(U,S=T,F) :-
      assert_rewrite_rule_3(S=T,U,F1),
      assert_rewrite_rule_3(T=S,U,F2),
      assert_rewrite_rule_6(F1,F2,F).
    assert_rewrite_rule_1((S->T),0) :-
      list_vars(T,Vs),
      assert_rewrite_rule_2(S,T,Vs),
      !.
    assert_rewrite_rule_1(S=T,0) :-
      list_vars(T,Vs),
      assert_rewrite_rule_2(S,T,Vs),
      !.
    assert_rewrite_rule_1(_,1).
    assert_rewrite_rule_2(S,T,[]).
    assert_rewrite_rule_2(S,T,[V|Vs]) :-
      count_occurrences(V,S,Ns),
      count_occurrences(V,T,Nt),
      Ns>=Nt,
      !,
      assert_rewrite_rule_2(S,T,Vs).
    assert_rewrite_rule_3(S=T,U,1) :-
      vars_tail(S=T,V),
      not(instance_rewrite_rule(S=T,V)),
      list_vars(T,Vs),
      assert_rewrite_rule_4(S=T,Vs,F),
      !,
      abolish_rewrite_caches,
      linearize_term(S=T,S1=T1,V1,V2),
      assertz(rwr(S1=T1,var(V1,V2,V),F,U)),
      print_rewrite_rule(rwr(S1=T1,var(V1,V2,V),F,U)).
    assert_rewrite_rule_3(_,_,0).
    assert_rewrite_rule_4(_,[],0).
    assert_rewrite_rule_4(S=T,[V|Vs],F) :-
      count_occurrences(V,S,Ns),
      Ns\==0,
      !,
      assert_rewrite_rule_5(S=T,[V|Vs],Ns,F).
    assert_rewrite_rule_5(S=T,[V|Vs],Ns,F) :-
      count_occurrences(V,T,Nt),
      Ns>=Nt,
      !,
      assert_rewrite_rule_4(S=T,Vs,F).
    assert_rewrite_rule_5(S=T,[_|Vs],_,1) :-
      !,
      assert_rewrite_rule_4(S=T,Vs,_).
    assert_rewrite_rule_6(1,_,1) :- !.
    assert_rewrite_rule_6(_,1,1) :- !.
    assert_rewrite_rule_6(_,_,0).

%%%
%%% Instance_rewrite_rule_ref determines if an existing rewrite rule is an
%%% instance of another existing rewrite rule.  We first check for duplicate
%%% to improve performance (at least under Quintus Prolog).
%%%
    instance_rewrite_rule_ref(Ref) :-
      const_list(V),
      clause(rwr(R,var(V1,V1,V),_,_),true,Ref),
      instance_rewrite_rule_ref_1(R,Ref),
      !.
    instance_rewrite_rule_ref_1((S->T),Ref) :-
      const_list(V),
      clause(rwr((S->T),var(V1,V1,V),_,_),true,Ref1),
      Ref1\==Ref,
      !.
    instance_rewrite_rule_ref_1((S->T),Ref) :-
      const_list(V),
      clause(rwr((T->S),var(V1,V1,V),_,_),true,Ref1),
      Ref1\==Ref,
      !.
    instance_rewrite_rule_ref_1(S=T,Ref) :-
      const_list(V),
      clause(rwr(S=T,var(V1,V1,V),_,_),true,Ref1),
      Ref1\==Ref,
      !.
    instance_rewrite_rule_ref_1((S->T),Ref) :-
      clause(rwr((S->T),var(V1,V1,_),_,_),true,Ref1),
      Ref1\==Ref,
      !.
    instance_rewrite_rule_ref_1((S->T),Ref) :-
      clause(rwr((T->S),var(V1,V1,_),_,_),true,Ref1),
      Ref1\==Ref,
      !.
    instance_rewrite_rule_ref_1(S=T,Ref) :-
      clause(rwr(S=T,var(V1,V1,_),_,_),true,Ref1),
      Ref1\==Ref,
      !.

%%%
%%% Instance_rewrite_rule determines if a rewrite rule is an instance of an
%%% existing rewrite rule.  We first check for duplicate to improve performance
%%% (at least under Quintus Prolog).
%%%
    instance_rewrite_rule(R,V) :-
      not(not(instance_rewrite_rule_1(R,V))),
      !.
    instance_rewrite_rule_1(R,V) :-
      const_list(V),
      instance_rewrite_rule_2(R),
      !.
    instance_rewrite_rule_2((S->T)) :-
      const_list(V),
      rwr((S->T),var(V1,V1,V),_,_),
      !.
    instance_rewrite_rule_2((S->T)) :-
      const_list(V),
      rwr((T->S),var(V1,V1,_),_,_),
      !.
    instance_rewrite_rule_2(S=T) :-
      const_list(V),
      rwr(S=T,var(V1,V1,_),_,_),
      !.
    instance_rewrite_rule_2((S->T)) :-
      rwr((S->T),var(V1,V1,_),_,_),
      !.
    instance_rewrite_rule_2((S->T)) :-
      rwr((T->S),var(V1,V1,_),_,_),
      !.
    instance_rewrite_rule_2(S=T) :-
      rwr(S=T,var(V1,V1,_),_,_),
      !.

%%%
%%% Lex_gt determines if a function or predicate is greater than another
%%% function or predicate.  The following ordering is used:
%%%   - user specified ordering
%%%   - arity (constants have arity 0)
%%%   - standard Prolog ordering of the symbol representing the function or
%%%     predicate
%%%
    lex_gt(S,Sa,T,Ta) :-
      rwo([S,Sa,T,Ta]),
      !.
    lex_gt(S,Sa,T,Ta) :-
      rwo([T,Ta,S,Sa]),
      !,
      fail.
    lex_gt(S,Sa,T,Ta) :-
      rwe([S,Sa,T,Ta]),
      !,
      fail.
    lex_gt(S,Sa,T,Ta) :-
      Sa>Ta,
      !.
    lex_gt(S,A,T,A) :-
      S@>T,
      !.

%%%
%%% Lex_eq determines if a function or predicate is equal to another function
%%% or predicate.  The following ordering is used:
%%%   - user specified ordering
%%%   - arity (constants have arity 0)
%%%   - standard Prolog ordering of the symbol representing the function or
%%%     predicate
%%%
    lex_eq(S,Sa,T,Ta) :-
      rwo([S,Sa,T,Ta]),
      !,
      fail.
    lex_eq(S,Sa,T,Ta) :-
      rwo([T,Ta,S,Sa]),
      !,
      fail.
    lex_eq(S,Sa,T,Ta) :-
      rwe([S,Sa,T,Ta]),
      !.
    lex_eq(F,A,F,A).

%%%
%%% Order_term determines the order (<,=,>,!) of two terms.
%%%
    order_term(T1,O,T2) :-
      term_ordering(lpo),
      !,
      order_term_lpo(T1,O,T2),
      !.
    order_term(_,_,_) :-
      term_ordering(X),
      !,
      write_line(5,'Invalid term ordering: ',X),
      abort.
    order_term(_,_,_) :-
      write_line(5,'No term ordering'),
      abort.

%%%
%%% Order_term_lpo determines the order (<,=,>,!) of two terms with respect to
%%% lexicographic path ordering.
%%%
    order_term_lpo(S,O,T) :-
      term_size_structure(S,SSize),
      term_size_structure(T,TSize),
      order_term_lpo_1(S,O,T,SSize,TSize).
    order_term_lpo_1(S,O,T,_,_) :-
      S==T,
      !,
      O='='.
    order_term_lpo_1(S,O,T,_,_) :-
      var(S),
      !,
      (occurs_check(T,S) -> (
        O='!'
      ); (
        O='<'
      )).
    order_term_lpo_1(S,O,T,_,_) :-
      var(T),
      !,
      (occurs_check(S,T) -> (
        O='!'
      ); (
        O='>'
      )).
    order_term_lpo_1(S,O,T,SSize,TSize) :-
      vars_tail({S,T},V),
      arg(1,SSize,Size1),
      arg(1,TSize,Size2),
      Size3 is (Size1*10000)+Size2,
      ((not(not((
          const_list(V),
          cached_term_order(Size3,S,T,V,O1),
          assert(cto_order(O1)))))) -> (
        retract(cto_order(O1))
      ); (
        Size4 is (Size2*10000)+Size1,
        vars_tail({T,S},V1),
        ((not(not((
            const_list(V1),
            cached_term_order(Size4,T,S,V1,O2),
            assert(cto_order(O2)))))) -> (
          retract(cto_order(O2)),
          order_term_lpo_9(O2,O1)
        ); (
          order_term_lpo_2(S,O1,T,SSize,TSize),
          counter(cached_term_order_count,N),
          cache_size(CacheSize),
          (N > CacheSize -> (
            write_line(0,'*** cleared cached_term_order: ',N),
            set_counter(cached_term_order_count,0),
            abolish(cached_term_order,5)
          ); true),
          Size5 is Size1+Size2,
          increment_counter(cached_term_order_count,Size5),
          assert(cached_term_order(Size3,S,T,V,O1))
        ))
      )),
      O=O1.
    order_term_lpo_2(S,O,T,SSize,TSize) :-
      functor(S,_,N),
      order_term_lpo_10(N,S,T,So,F,SSize,TSize),
      !,
      order_term_lpo_3(F,S,O,T,So,SSize,TSize).
    order_term_lpo_3(1,_,>,_,_,_,_) :- !.
    order_term_lpo_3(0,S,O,T,So,SSize,TSize) :-
      functor(T,_,N),
      order_term_lpo_10(N,T,S,To,F,TSize,SSize),
      !,
      order_term_lpo_4(F,S,O,T,So,To,SSize,TSize).
    order_term_lpo_4(1,_,<,_,_,_,_,_) :- !.
    order_term_lpo_4(0,S,O,T,So,To,SSize,TSize) :-
      functor(S,Sf,Sn),
      functor(T,Tf,Tn),
      lex_eq(Sf,Sn,Tf,Tn),
      !,
      order_term_lpo_5(Sn,S,O,T,So,To,SSize,TSize).
    order_term_lpo_4(0,S,O,T,So,To,_,_) :-
      functor(S,Sf,Sn),
      functor(T,Tf,Tn),
      lex_gt(Sf,Sn,Tf,Tn),
      !,
      order_term_lpo_8(To,O).
    order_term_lpo_4(0,S,O,T,So,To,_,_) :-
      functor(S,Sf,Sn),
      functor(T,Tf,Tn),
      lex_gt(Tf,Tn,Sf,Sn),
      !,
      order_term_lpo_8(So,O1),
      order_term_lpo_9(O1,O).
    order_term_lpo_4(0,_,!,_,_,_,_,_).
    order_term_lpo_5(0,_,O,_,_,_,_,_) :-
      !,
      O='='.
    order_term_lpo_5(N,S,O,T,[_|So],[_|To],SSize,TSize) :-
      functor(S,_,N1),
      N2 is N1-N+1,
      arg(N2,S,Si),
      arg(N2,T,Ti),
      N3 is N2+1,
      arg(N3,SSize,SiSize),
      arg(N3,TSize,TiSize),
      order_term_lpo_1(Si,O1,Ti,SiSize,TiSize),
      order_term_lpo_6(O1,N,S,T,So,To,O,SSize,TSize).
    order_term_lpo_6(=,N,S,T,So,To,O,SSize,TSize) :-
      N1 is N-1,
      order_term_lpo_5(N1,S,O,T,So,To,SSize,TSize).
    order_term_lpo_6(!,_,_,_,_,_,!,_,_).
    order_term_lpo_6(>,_,_,_,_,To,O,_,_) :-
      (order_term_lpo_7(To) -> (
        O='>'
      ); (
        O='!'
      )).
    order_term_lpo_6(<,_,_,_,So,_,O,_,_) :-
      (order_term_lpo_7(So) -> (
        O='<'
      ); (
        O='!'
      )).
    order_term_lpo_7([]) :- !.
    order_term_lpo_7([<|So]) :-
      order_term_lpo_7(So).
    order_term_lpo_8([],O) :-
      !,
      O='>'.
    order_term_lpo_8([!|_],O) :-
      !,
      O='!'.
    order_term_lpo_8([<|So],O) :-
      order_term_lpo_8(So,O).
    order_term_lpo_9(>,O) :-
      !,
      O='<'.
    order_term_lpo_9(<,O) :-
      !,
      O='>'.
    order_term_lpo_9(O,O).
    order_term_lpo_10(0,_,_,[],0,_,_) :- !.
    order_term_lpo_10(N,S,T,[O|So],F,SSize,TSize) :-
      functor(S,_,N1),
      N2 is N1-N+1,
      arg(N2,S,Si),
      N3 is N2+1,
      arg(N3,SSize,SiSize),
      order_term_lpo_1(Si,O,T,SiSize,TSize),
      order_term_lpo_11(O,N,S,T,So,F,SSize,TSize).
    order_term_lpo_11(>,_,_,_,_,1,_,_) :- !.
    order_term_lpo_11(=,_,_,_,_,1,_,_) :- !.
    order_term_lpo_11(_,N,S,T,So,F,SSize,TSize) :-
      N1 is N-1,
      order_term_lpo_10(N1,S,T,So,F,SSize,TSize).

%%%
%%% Assert_saved_term_order asserts intermediate term ordering data into the
%%% database.
%%%
    assert_saved_term_order(S,T,V,F) :-
      memoize_term_order,
      !,
      assert(saved_term_order(S,T,V,F)),
      !.
    assert_saved_term_order(_,_,_,_) :- !.

%%%
%%% Check_saved_term_order checks to see if the ordering as previously been
%%% computed.
      check_saved_term_order(T1,T2,V,F) :-
        memoize_term_order,
        not(not(check_saved_term_order_1(T1,T2,V))),
        retract(csto_temp(F)),
        !.
      check_saved_term_order_1(T1,T2,V) :-
        const_list(V),
        saved_term_order(T1,T2,_,1),
        asserta(csto_temp(1)),
        !.
      check_saved_term_order_1(T1,T2,V) :-
        const_list(V),
        saved_term_order(T1,T2,V,0),
        asserta(csto_temp(0)),
        !.

%%%
%%% Print_rewrite_rule prints a rewrite rule.
%%%
    print_rewrite_rule(_) :-
      not(outrwr),
      !.
    print_rewrite_rule(R) :-
      not(not(print_rewrite_rule1(R))),
      !.
    print_rewrite_rule1(rwr((S->T),var(V1,V1,V),F,U)) :-
      var_list(V),
      write_line(10,'rewrite rule: ',S,'->',T),
      !.
    print_rewrite_rule1(rwr(S=T,var(V1,V1,V),F,U)) :-
      var_list(V),
      write_line(10,'rewrite rule: ',S,'=',T),
      !.

%%%
%%% Orient_equation orients an equation.
%%%
    orient_equation(S=T,T=S) :-
      order_term(T,>,S),
      !.
    orient_equation(L,L).

%%%
%%% Assert_rewrite_rule_equations asserts the corresponding equation for each
%%% rewrite rule if the equation is not already asserted.
%%%
    assert_rewrite_rule_equations :-
      rwr((S->T),var(V1,V1,V),_,_),
      clause_size([S=T],CSize),
      assert_rewrite_rule_equations_1(CSize,[S=T],C,V),
      fail.
    assert_rewrite_rule_equations :-
      rwr(S=T,var(V1,V1,V),_,_),
      clause_size([S=T],CSize),
      assert_rewrite_rule_equations_1(CSize,[S=T],C,V),
      fail.
    assert_rewrite_rule_equations.
    assert_rewrite_rule_equations_1(CSize,[S=T],C,V) :-
      not(duplicate_clause_C(CSize,[S=T],V)),
      vars_literals([S=T],W),
      compute_V_lits(W,0,NLits),
      linearize_term([S=T],C,V1,V2),
      set_user_support(C,S1),
      set_sr_status(S1,C,Sp,Ds),
      calculate_priority_clause(C,Sp,Ds,Pr),
      assert_rewrite_rule_equations_2(Pr),
      list_of_Ns(C,0,Dis),
      assertz(sent_C(cl(CSize,NLits,by(C,V1,V2,V,W),0,Sp,Ds,0,Dis,Pr))).
    assert_rewrite_rule_equations_2(Pr) :-
      priority_bound(PrioBound),
      !,
      check_prioritybound(Pr,PrioBound).
    assert_rewrite_rule_equations_2(_).

%%%
%%% Set_user_support set the user support flag as follows:
%%%   if current support includes user support then
%%%     if the user support is "o" then
%%%       if the clause is a unit clause then
%%%         set user support flag to 1
%%%       else set user support flag to 0
%%%     else set user support flag to 0
%%%   else set user support flag to 1
%%%
    set_user_support(C,S1) :-
      current_support(sup(1,_,_,_)),
      !,
      set_user_support_1(C,S1).
    set_user_support(_,1).
    set_user_support_1(C,S1) :-
      user_support(o),
      !,
      set_user_support_2(C,S1).
    set_user_support_1(_,0).
    set_user_support_2([L],1) :- !.
    set_user_support_2(_,0).

%%%
%%% remove_rewrite_rule(E)
%%%   input
%%%     E  : equation
%%%
    remove_rewrite_rule(E) :-
      vars_tail(E,V),
      assert(dont_use_rewrite_rule_outer(E,V)).

%%%
%%% restore_rewrite_rule(E)
%%%   input
%%%     E : equation
%%%
    restore_rewrite_rule(E) :-
      vars_tail(E,V),
      retract(dont_use_rewrite_rule_outer(E,V)).

%%%
%%% print_rewrite_with_constraint(T,Cts) - prints a term and its constrained
%%% normal forms
%%%   input
%%%     T   : term
%%%     Cts : set of term/flag/constraint triples representing the constrained
%%%           normal forms of T
%%%
    print_rewrite_with_constraint(_,_) :-
      not(outrwt),
      !.
    print_rewrite_with_constraint(T,Cts) :-
      not(not(print_rewrite_with_constraint_1(T,Cts))).
    print_rewrite_with_constraint_1(T,Cts) :-
      vars_tail(T,V),
      var_list(V),
      write_line(10,'rewriting:'),
      write_line(13,'orig: ',T),
      print_rewrite_with_constraint_2(Cts).
    print_rewrite_with_constraint_2([]) :- !.
    print_rewrite_with_constraint_2([[T,_,Con]|Cts1]) :-
      write_line(13,'new:  ',T,' ',Con),
      print_rewrite_with_constraint_3(Cts1).
    print_rewrite_with_constraint_3([]) :- !.
    print_rewrite_with_constraint_3([[T,_,Con]|Cts1]) :-
      write_line(13,'      ',T,' ',Con),
      print_rewrite_with_constraint_3(Cts1).

%%%
%%% rewrite_clause_with_constraint(C,Sp,Ds,Con,Cts)
%%%   input
%%%     C   : clause
%%%     Sp  : support data for computing priority
%%%     Ds  : distance data for computing priority
%%%     Con : constraint
%%%   output
%%%     Cts : set of simplified clause/flag/constraint triples obtained by
%%%           rewriting C under the constraint Con.  Flag is set as follows:
%%%             0 -- clause fully rewritten
%%%             1 -- rewrite terminated early due to priority
%%%   notes
%%%     If Sp is uninstantiated, the priority is not checked after using a
%%%       marked equational rule.
%%%
    rewrite_clause_with_constraint(C,_,_,Con,[[C,0,Con]]) :-
      not(rwr(_,_,_,_)),
      !.
    rewrite_clause_with_constraint(C,Sp,Ds,Con,Cts) :-
      (precompute_constraints -> (
        rewrite_clause_with_constraint_1(C,[],Vss1),
        identical_delete_all_duplicates(Vss1,Vss2),
        rewrite_clause_with_constraint_5(Vss2,Conss),
        bagof1(Con1,rewrite_clause_with_constraint_8(Conss,[],Con1),Cons),
        rewrite_clause_with_constraint_9(Cons,C,Sp,Ds,Con,[],Cts)
      ); (
        rewrite_clause_with_constraint_9([[]],C,Sp,Ds,Con,[],Cts)
      )).
    rewrite_clause_with_constraint_1([],Vss,Vss) :- !.
    rewrite_clause_with_constraint_1([not S=T|C],Vss1,Vss2) :-
      restricted_rewrite,
      !,
      (nonvar(S) -> (
        functor(S,_,N),
        rewrite_clause_with_constraint_4(N,S,[],Vss3)
      ); (
        Vss3=[]
      )),
      (nonvar(T) -> (
        rewrite_clause_with_constraint_2(T,Vss4)
      ); (
        Vss4=[]
      )),
      append(Vss3,Vss4,Vss5),
      append(Vss1,Vss5,Vss6),
      rewrite_clause_with_constraint_1(C,Vss6,Vss2).
    rewrite_clause_with_constraint_1([not L|C],Vss1,Vss2) :-
      !,
      functor(L,_,N),
      rewrite_clause_with_constraint_4(N,L,[],Vss3),
      append(Vss1,Vss3,Vss4),
      rewrite_clause_with_constraint_1(C,Vss4,Vss2).
    rewrite_clause_with_constraint_1([L|C],Vss1,Vss2) :-
      functor(L,_,N),
      rewrite_clause_with_constraint_4(N,L,[],Vss3),
      append(Vss1,Vss3,Vss4),
      rewrite_clause_with_constraint_1(C,Vss4,Vss2).
    rewrite_clause_with_constraint_2(T,Vss) :-
      (var(T) -> (
        Vss=[]
      ); (
        vars_tail(T,V),
        (not(not((
            const_list(V),
            (rwr((T->_),var(V1,V1,_),_,_); rwr(T=_,var(V1,V1,_),_,_))))) -> (
          list_vars(T,Vs),
          (Vs=[_] -> (
            Vss=[]
          ); (
            Vss=[Vs]
          ))
        ); (
          functor(T,_,N),
          rewrite_clause_with_constraint_3(N,T,[],Vss)
        ))
      )).
    rewrite_clause_with_constraint_3(0,_,Vss,Vss) :- !.
    rewrite_clause_with_constraint_3(N,T,Vss1,Vss2) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,A),
      rewrite_clause_with_constraint_2(A,Vss3),
      append(Vss1,Vss3,Vss4),
      N3 is N-1,
      rewrite_clause_with_constraint_3(N3,T,Vss4,Vss2).
    rewrite_clause_with_constraint_4(0,_,Vss,Vss) :- !.
    rewrite_clause_with_constraint_4(N,L,Vss1,Vss2) :-
      functor(L,_,N1),
      N2 is N1-N+1,
      arg(N2,L,Li),
      N3 is N-1,
      (var(Li) -> (
        rewrite_clause_with_constraint_4(N3,L,Vss1,Vss2)
      ); (
        rewrite_clause_with_constraint_2(Li,Vss3),
        append(Vss1,Vss3,Vss4),
        rewrite_clause_with_constraint_4(N3,L,Vss4,Vss2)
      )).
    rewrite_clause_with_constraint_5([],[]) :- !.
    rewrite_clause_with_constraint_5([Vs|Vss],[Cons|Conss]) :-
      (Vs==[] -> (
        Cons=[]
      ); (
        permutations(Vs,P),
        bagof(Con1,rewrite_clause_with_constraint_6(P,Con1),Cons)
      )),
      rewrite_clause_with_constraint_5(Vss,Conss).
    rewrite_clause_with_constraint_6(P,Con) :-
      member(L,P),
      rewrite_clause_with_constraint_7(L,Con).
    rewrite_clause_with_constraint_7([_],[]) :- !.
    rewrite_clause_with_constraint_7([X,Y|Z],[X>Y|Con]) :-
      rewrite_clause_with_constraint_7([Y|Z],Con).
    rewrite_clause_with_constraint_8([],Con1,Con2) :-
      identical_delete_all_duplicates(Con1,Con2).
    rewrite_clause_with_constraint_8([Cons|Conss],Con1,Con2) :-
      (Cons==[] -> (
        rewrite_clause_with_constraint_8(Conss,Con1,Con2)
      ); (
        member(Con3,Cons),
        append(Con1,Con3,Con4),
        rewrite_clause_with_constraint_8(Conss,Con4,Con2)
      )).
    rewrite_clause_with_constraint_9([],_,_,_,_,Cts,Cts) :- !.
    rewrite_clause_with_constraint_9([Con1|Cons],C,Sp,Ds,Con2,Cts1,Cts2) :-
      (Con2==[] -> (
        (constraint_consistent(Con1) -> (
          rewrite_clause_with_constraint_10(C,Sp,Ds,Con1,Cts3)
        ); (
          Cts3=[]
        ))
      ); (
        append(Con2,Con1,Con3),
        identical_delete_all_duplicates(Con3,Con4),
        (constraint_consistent(Con4) -> (
          rewrite_clause_with_constraint_10(C,Sp,Ds,Con4,Cts3)
        ); (
          Cts3=[]
        ))
      )),
      append(Cts1,Cts3,Cts4),
      rewrite_clause_with_constraint_9(Cons,C,Sp,Ds,Con2,Cts4,Cts2).
    rewrite_clause_with_constraint_10([],_,_,Con,[[[],0,Con]]) :- !.
    rewrite_clause_with_constraint_10([L|Ls],Sp,Ds,Con,Cts) :-
      rewrite_lit_with_constraint(L,Sp,Ds,Con,Cts1),
      rewrite_clause_with_constraint_11(Cts1,Ls,Sp,Ds,[],Cts).
    rewrite_clause_with_constraint_11([],_,_,_,Cts,Cts) :- !.
    rewrite_clause_with_constraint_11([[L,0,Con]|Cts1],Ls,Sp,Ds,Cts2,Cts3) :-
      !,
      rewrite_clause_with_constraint_10(Ls,Sp,Ds,Con,Cts4),
      rewrite_clause_with_constraint_12(Cts4,L,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_clause_with_constraint_11(Cts1,Ls,Sp,Ds,Cts6,Cts3).
    rewrite_clause_with_constraint_11([[L,1,Con]|Cts1],Ls,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[[[L|Ls],1,Con]],Cts4),
      rewrite_clause_with_constraint_11(Cts1,Ls,Sp,Ds,Cts4,Cts3).
    rewrite_clause_with_constraint_12([],_,[]) :- !.
    rewrite_clause_with_constraint_12([[L1,F,Con]|Cts1],L2,
        [[[L2|L1],F,Con]|Cts2]) :-
      rewrite_clause_with_constraint_12(Cts1,L2,Cts2).

%%%
%%% rewrite_lit_with_constraint(L,Sp,Ds,Con,Cts)
%%%   input
%%%     L   : literal
%%%     Sp  : support data for computing priority
%%%     Ds  : distance data for computing priority
%%%     Con : constraint
%%%   output
%%%     Cts : set of simplified literal/flag/constraint triples obtained by
%%%           rewriting L under the constraint Con.  Flag is set as follows:
%%%             0 -- literal fully rewritten
%%%             1 -- rewrite terminated early due to priority
%%%   notes
%%%     If Sp is uninstantiated, the priority is not checked after using a
%%%       marked equational rule.
%%%
    rewrite_lit_with_constraint(S=T,Sp,Ds,Con,Cts) :-
      restricted_rewrite,
      !,
      order_term(S,O,T),
      (O=='>' -> (
        rewrite_term_with_constraint(T,Sp,Ds,Con,Cts1),
        rewrite_lit_with_constraint_1(Cts1,S,Sp,Ds,[],Cts2)
      ); (O=='<' -> (
        rewrite_term_with_constraint(S,Sp,Ds,Con,Cts1),
        rewrite_lit_with_constraint_1(Cts1,T,Sp,Ds,[],Cts2)
      ); (
        rewrite_term_with_constraint(S,Sp,Ds,Con,Cts1),
        rewrite_lit_with_constraint_6(Cts1,T,Sp,Ds,[],Cts2)
      ))),
      rewrite_lit_with_constraint_7(Cts2,Cts).
    rewrite_lit_with_constraint(S=T,Sp,Ds,Con,Cts) :-
      !,
      remove_rewrite_rule(S=T),
      rewrite_term_with_constraint(S,Sp,Ds,Con,Cts1),
      restore_rewrite_rule(S=T),
      rewrite_lit_with_constraint_9(Cts1,S,T,Sp,Ds,[],Cts2),
      rewrite_lit_with_constraint_7(Cts2,Cts).
    rewrite_lit_with_constraint(not S=T,Sp,Ds,Con,Cts) :-
      restricted_rewrite,
      !,
      rewrite_term_args_only_with_constraint(S,Sp,Ds,Con,Cts1),
      rewrite_lit_with_constraint_6(Cts1,T,Sp,Ds,[],Cts2),
      rewrite_lit_with_constraint_12(Cts2,Cts).
    rewrite_lit_with_constraint(not L,Sp,Ds,Con,Cts) :-
      !,
      rewrite_term_with_constraint(L,Sp,Ds,Con,Cts1),
      rewrite_lit_with_constraint_12(Cts1,Cts).
    rewrite_lit_with_constraint(L,Sp,Ds,Con,Cts) :-
      rewrite_term_with_constraint(L,Sp,Ds,Con,Cts).
    rewrite_lit_with_constraint_1([],_,_,_,Cts,Cts) :- !.
    rewrite_lit_with_constraint_1([[T,0,Con]|Cts1],S,Sp,Ds,Cts2,Cts3) :-
      vars_tail(S,V),
      rewrite_lit_with_constraint_2(S,V,S1),
      order_term(S1,<,T),
      !,
      rewrite_term_with_constraint(S1,Sp,Ds,Con,Cts4),
      rewrite_lit_with_constraint_3(Cts4,T,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_lit_with_constraint_1(Cts1,S,Sp,Ds,Cts6,Cts3).
    rewrite_lit_with_constraint_1([[T,0,Con]|Cts1],S,Sp,Ds,Cts2,Cts3) :-
      !,
      rewrite_term_args_only_with_constraint(S,Sp,Ds,Con,Cts4),
      rewrite_lit_with_constraint_4(Cts4,S,T,Sp,Ds,[],Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_lit_with_constraint_1(Cts1,S,Sp,Ds,Cts6,Cts3).
    rewrite_lit_with_constraint_1([[T,1,Con]|Cts1],S,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[[S=T,1,Con]],Cts4),
      rewrite_lit_with_constraint_1(Cts1,S,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_2(S1,V,S2) :-
      rwr((S1->S2),var(V1,V2,_),_,_),
      unify_lists(V1,V2),
      not(not(const_list(V))).
    rewrite_lit_with_constraint_2(S1,V,S2) :-
      equational_rewrite,
      rwr(S1=S2,var(V1,V2,_),_,_),
      unify_lists(V1,V2),
      not(not(const_list(V))),
      order_term(S1,>,S2).
    rewrite_lit_with_constraint_3([],_,[]) :- !.
    rewrite_lit_with_constraint_3([[S,F,Con]|Cts1],T,[[S=T,F,Con]|Cts2]) :-
      rewrite_lit_with_constraint_3(Cts1,T,Cts2).
    rewrite_lit_with_constraint_4([],_,_,_,_,Cts,Cts) :- !.
    rewrite_lit_with_constraint_4([[S1,0,Con]|Cts1],S2,T,Sp,Ds,Cts2,Cts3) :-
      S1==S2,
      !,
      append(Cts2,[[S2=T,0,Con]],Cts4),
      rewrite_lit_with_constraint_4(Cts1,S2,T,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_4([[S1,0,Con]|Cts1],S2,T,Sp,Ds,Cts2,Cts3) :-
      !,
      rewrite_term_with_constraint(S1,Sp,Ds,Con,Cts4),
      rewrite_lit_with_constraint_5(Cts4,T,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_lit_with_constraint_4(Cts1,S2,T,Sp,Ds,Cts6,Cts3).
    rewrite_lit_with_constraint_4([[S1,1,Con]|Cts1],S2,T,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[[S1=T,1,Con]],Cts4),
      rewrite_lit_with_constraint_4(Cts1,S2,T,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_5([],_,[]) :- !.
    rewrite_lit_with_constraint_5([[S,F,Con]|Cts1],T,[[S=T,F,Con]|Cts2]) :-
      rewrite_lit_with_constraint_5(Cts1,T,Cts2).
    rewrite_lit_with_constraint_6([],_,_,_,Cts,Cts) :- !.
    rewrite_lit_with_constraint_6([[S,0,Con]|Cts1],T,Sp,Ds,Cts2,Cts3) :-
      !,
      rewrite_term_with_constraint(T,Sp,Ds,Con,Cts4),
      rewrite_lit_with_constraint_8(Cts4,S,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_lit_with_constraint_6(Cts1,T,Sp,Ds,Cts6,Cts3).
    rewrite_lit_with_constraint_6([[S,1,Con]|Cts1],T,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[[S=T,1,Con]],Cts4),
      rewrite_lit_with_constraint_6(Cts1,T,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_7([],[]) :- !.
    rewrite_lit_with_constraint_7([[S=T,F,Con]|Cts1],[[E,F,Con]|Cts2]) :-
      order_term(S,O,T),
      (O=='<' -> (
        E=(T=S)
      ); (
        E=(S=T)
      )),
      rewrite_lit_with_constraint_7(Cts1,Cts2).
    rewrite_lit_with_constraint_8([],_,[]) :- !.
    rewrite_lit_with_constraint_8([[T,F,Con]|Cts1],S,[[S=T,F,Con]|Cts2]) :-
      rewrite_lit_with_constraint_8(Cts1,S,Cts2).
    rewrite_lit_with_constraint_9([],_,_,_,_,Cts,Cts) :- !.
    rewrite_lit_with_constraint_9([[S1,0,Con]|Cts1],S2,T,Sp,Ds,Cts2,Cts3) :-
      !,
      (S1\==S2 -> (
        rewrite_term_with_constraint(T,Sp,Ds,Con,Cts4),
        rewrite_lit_with_constraint_8(Cts4,S1,Cts5),
        append(Cts2,Cts5,Cts6),
        rewrite_lit_with_constraint_9(Cts1,S2,T,Sp,Ds,Cts6,Cts3)
      ); (
        remove_rewrite_rule(T=S2),
        rewrite_term_with_constraint(T,Sp,Ds,Con,Cts4),
        restore_rewrite_rule(T=S2),
        rewrite_lit_with_constraint_8(Cts4,S1,Cts5),
        rewrite_lit_with_constraint_10(Cts5,T,Sp,Ds,[],Cts6),
        append(Cts2,Cts6,Cts7),
        rewrite_lit_with_constraint_9(Cts1,S2,T,Sp,Ds,Cts7,Cts3)
      )).
    rewrite_lit_with_constraint_9([[S1,1,Con]|Cts1],S2,T,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[[S1=T,1,Con]],Cts4),
      rewrite_lit_with_constraint_9(Cts1,S2,T,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_10([],_,_,_,Cts,Cts) :- !.
    rewrite_lit_with_constraint_10([[S=T1,0,Con]|Cts1],T2,Sp,Ds,Cts2,Cts3) :-
      T1\==T2,
      !,
      rewrite_term_with_constraint(S,Sp,Ds,Con,Cts4),
      rewrite_lit_with_constraint_11(Cts4,T1,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_lit_with_constraint_10(Cts1,T2,Sp,Ds,Cts6,Cts3).
    rewrite_lit_with_constraint_10([Ct|Cts1],T,Sp,Ds,Cts2,Cts3) :-
      append(Cts2,[Ct],Cts4),
      rewrite_lit_with_constraint_10(Cts1,T,Sp,Ds,Cts4,Cts3).
    rewrite_lit_with_constraint_11([],_,[]) :- !.
    rewrite_lit_with_constraint_11([[S,F,Con]|Cts1],T,[[S=T,F,Con]|Cts2]) :-
      rewrite_lit_with_constraint_11(Cts1,T,Cts2).
    rewrite_lit_with_constraint_12([],[]) :- !.
    rewrite_lit_with_constraint_12([[L,F,Con]|Cts1],
        [[not L,F,Con]|Cts2]) :-
      rewrite_lit_with_constraint_12(Cts1,Cts2).

%%%
%%% rewrite_term_with_constraint(T,Sp,Ds,Con,Cts)
%%%   input
%%%     T   : term
%%%     Sp  : support data for computing priority
%%%     Ds  : distance data for computing priority
%%%     Con : constraint
%%%   output
%%%     Cts : set of simplified term/flag/constraint triples obtained by
%%%           rewriting T under the constraint C.  Flag is set as follows:
%%%             0 -- term fully rewritten
%%%             1 -- rewrite terminated early due to priority
%%%   notes
%%%     If Sp is uninstantiated, the priority is not checked after using a
%%%       marked equational rule.
%%%
    rewrite_term_with_constraint(T,Sp,Ds,Con,Cts) :-
      (var(T) -> (
        Cts=[[T,0,Con]]
      ); (
        abolish(term_rewritten,0),
        vars_tail({T,Con},V),
        rewrite_term_with_constraint_1(T,Sp,Ds,V,Con,Cts)
      )).
    rewrite_term_with_constraint_1(T,Sp,Ds,V,Con,Cts) :-
%      not(not((
%        var_list(V),
%        write('*** entered rewrite_term_with_constraint_1('),
%        write(T),
%        write(','),
%        (var(Sp) -> (
%          write('Sp')
%        ); (
%          write(Sp)
%        )),
%        write(','),
%        (var(Ds) -> (
%          write('Ds')
%        ); (
%          write(Ds)
%        )),
%        write(',V,'),
%        write(Con),
%        write(',Cts)'),
%        write_line(0,'')
%      ))),
      (var(T)  -> (
        Cts=[[T,0,Con]]
      ); (
        term_size_structure(T,TSize),
        term_size(Con,Size2),
        ((term_rewritten; (not(not((const_list(V),
            not(dont_use_rewrite_rule_outer(T=_,V))))))) -> (
          arg(1,TSize,Size1),
          Size3 is (Size1*10000)+Size2,
          ((cached_rewrite(Size3,T,Con,var(V1,V2,V3),Cts),
              not(not(const_list(V))),
              not(not(const_list(V3))),
              not(not((V1=V2,const_list(V))))) -> (
            assert(rewrite_found)
          ); (
            Caching_allowed=1
          ))
        ); (
          Caching_allowed=0
       )),
        (rewrite_found -> (
          abolish(rewrite_found,0)
        ); (
          (not(term_rewritten) -> (
            Term_not_rewritten=1
          ); (
            Term_not_rewritten=0
          )),
          rewrite_term_with_constraint_2(T,Sp,Ds,V,Con,TSize,Size2,Cts1),
         ((Cts1\==[[T,0,Con]], Cts1\==[[T,1,Con]]) -> (
            assert_once(term_rewritten)
          ); true),
          (rtwc_stop -> (
            abolish(rtwc_stop,0),
            Cts1=[[T1,F,Con1]],
            (F==0 -> (
             rewrite_term_with_constraint_1(T1,Sp,Ds,V,Con1,Cts)
            ); (
              Cts=Cts1
            ))
          ); (
            (Cts1==[] -> (
              Cts=[[T,0,Con]]
            ); (
              simplify_constraint_triples(Cts1,Cts2),
              rewrite_term_with_constraint_7(Cts2,Con,Cons1),
              negate_constraints(Cons1,Cons2),
              (Con==[] -> (
                Cons3=Cons2
              ); (
               rewrite_term_with_constraint_8(Cons2,Con,Cons3)
              )),
              rewrite_term_with_constraint_9(Cons3,T,Cts3),
              ((term_rewritten, Term_not_rewritten==1) -> (
                rewrite_term_with_constraint_10(Cts2,Sp,Ds,V,[],Cts4),
                abolish(term_rewritten,0),
                rewrite_term_with_constraint_10(Cts3,Sp,Ds,V,[],Cts5),
                assert(term_rewritten),
                append(Cts4,Cts5,Cts)
              ); (
                append(Cts2,Cts3,Cts4),
                rewrite_term_with_constraint_10(Cts4,Sp,Ds,V,[],Cts)
              ))
            ))
          )),
          (Caching_allowed==1 -> (
            counter(cached_rewrite_count,N),
            cache_size(CacheSize),
            (N > CacheSize -> (
              write_line(0,'*** cleared cached_rewrite: ',N),
              set_counter(cached_rewrite_count,0),
              abolish(cached_rewrite,5)
            ); true),
            term_size(Cts,Size4),
            Size5 is Size1+Size2+Size4,
            increment_counter(cached_rewrite_count,Size5),
            linearize_term({T,Con},{T2,Con2},V4,V5),
            assert(cached_rewrite(Size3,T2,Con2,var(V4,V5,V),Cts))
          ); true)
        ))
      )).
    rewrite_term_with_constraint_2(T,Sp,Ds,V,Con,TSize,Size2,Cts) :-
%      not(not((
%        var_list(V),
%        write('*** entered rewrite_term_with_constraint_2('),
%        write(T),
%        write(','),
%        (var(Sp) -> (
%          write('Sp')
%        ); (
%          write(Sp)
%        )),
%        write(','),
%        (var(Ds) -> (
%          write('Ds')
%        ); (
%          write(Ds)
%        )),
%        write(',V,'),
%        write(Con),
%        write(','),
%        write(TSize),
%        write(','),
%        write(Size2),
%        write(',Cts)'),
%        write_line(0,'')
%      ))),
      (var(T) -> (
        Cts=[]
      ); (
        ((term_rewritten; (not(not((const_list(V),
            not(dont_use_rewrite_rule_outer(T=_,V))))))) -> (
          arg(1,TSize,Size1),
          Size3 is (Size1*10000)+Size2,
          ((cached_subterm_rewrite(Size3,T,Con,var(V1,V2,V3),Cts,Stop),
              not(not(const_list(V))),
              not(not(const_list(V3))),
              not(not((V1=V2,const_list(V))))) -> (
            assert(subterm_rewrite_found),
            (Stop==1 -> (
              assert_once(rtwc_stop)
            ); true)
          ); (
            Caching_allowed=1
          ))
        ); (
          Caching_allowed=0
        )),
        (subterm_rewrite_found -> (
          abolish(subterm_rewrite_found,0)
        ); (
          bagof1(R,rewrite_term_with_constraint_3(T,V,R),Rs),
          rewrite_term_with_constraint_4(Rs,Sp,Ds,Con,Cts1),
          (rtwc_stop -> (
            tail(Cts1,Ct),
            Cts=[Ct]
          ); (
            functor(T,_,N1),
            rewrite_term_with_constraint_5(N1,T,Sp,Ds,V,Con,TSize,Size2,[],
              Cts2),
            (rtwc_stop -> (
              Cts=Cts2
            ); (
              append(Cts1,Cts2,Cts)
            ))
          )),
          (Caching_allowed==1 -> (
            counter(cached_subterm_rewrite_count,N2),
            cache_size(CacheSize),
            (N2 > CacheSize -> (
              write_line(0,'*** cleared cached_subterm_rewrite: ',N2),
              set_counter(cached_subterm_rewrite_count,0),
              abolish(cached_subterm_rewrite,6)
            ); true),
            term_size(Cts,Size4),
            Size5 is Size1+Size2+Size4,
            increment_counter(cached_subterm_rewrite_count,Size5),
            linearize_term({T,Con},{T1,Con1},V4,V5),
            (rtwc_stop -> (
              assert(cached_subterm_rewrite(Size3,T1,Con1,var(V4,V5,V),Cts,1))
            ); (
              assert(cached_subterm_rewrite(Size3,T1,Con1,var(V4,V5,V),Cts,0))
            ))
          ); true)
        ))
      )).
    rewrite_term_with_constraint_3(T,V,{(T->T1),F}) :-
      rwr((T->T1),var(V1,V2,V3),F,_),
      unify_lists(V1,V2),
      not(not(const_list(V))),
      (term_rewritten;
        not(const_list(V3));
        (not(not((
          const_list(V3),
          not(dont_use_rewrite_rule_outer(T=T1,V3))
        ))))
      ),
      !.
    rewrite_term_with_constraint_3(T,V,{T=T1,F}) :-
      rwr((T=T1),var(V1,V2,V3),F,_),
      unify_lists(V1,V2),
      not(not(const_list(V))),
      (term_rewritten;
        not(const_list(V3));
        (not(not((
          const_list(V3),
          not(dont_use_rewrite_rule_outer(T=T1,V3))
        ))))
      ).
    rewrite_term_with_constraint_4([],_,_,_,[]) :- !.
    rewrite_term_with_constraint_4([{(T->T1),F}|_],Sp,Ds,Con,[Ct]) :-
      !,
      assert(rtwc_stop),
      ((F==1, nonvar(Sp), priority_bound(PrioBound)) -> (
        calculate_priority_clause([T1],Sp,Ds,Pr),
        (check_prioritybound(Pr,PrioBound) -> (
          Ct=[T1,0,Con]
        ); (
          Ct=[T1,1,Con]
        ))
      ); (
        Ct=[T1,0,Con]
      )).
    rewrite_term_with_constraint_4([{T=T1,F}|Rs],Sp,Ds,Con,Cts) :-
      !,
      order_term(T,O,T1),
      ((O=='>'; (O=='!', implies_constraint(Con,[T>T1]))) -> (
        assert(rtwc_stop),
        ((F==1, nonvar(Sp), priority_bound(PrioBound)) -> (
          calculate_priority_clause([T1],Sp,Ds,Pr),
          (check_prioritybound(Pr,PrioBound) -> (
            Cts=[[T1,0,Con]]
          ); (
            Cts=[[T1,1,Con]]
          ))
        ); (
          Cts=[[T1,0,Con]]
        ))
      ); (
        ((not(precompute_constraints), O=='!',
            constraint_consistent([T>T1|Con])) -> (
          append(Con,[T>T1],Con1),
          ((F==1, nonvar(Sp), priority_bound(PrioBound)) -> (
            calculate_priority_clause([T1],Sp,Ds,Pr),
            (check_prioritybound(Pr,PrioBound) -> (
              Ct=[T1,0,Con1]
            ); (
              Ct=[T1,1,Con1]
            ))
          ); (
            Ct=[T1,0,Con1]
          )),
          rewrite_term_with_constraint_4(Rs,Sp,Ds,Con,Cts1),
          Cts=[Ct|Cts1]
        ); (
          rewrite_term_with_constraint_4(Rs,Sp,Ds,Con,Cts)
        ))
      )).
    rewrite_term_with_constraint_5(0,_,_,_,_,_,_,_,Cts,Cts) :- !.
    rewrite_term_with_constraint_5(N,T,Sp,Ds,V,Con,TSize,Size2,Cts1,Cts2) :-
      arg(N,T,Ti),
      N1 is N+1,
      arg(N1,TSize,TiSize),
      rewrite_term_with_constraint_2(Ti,Sp,Ds,V,Con,TiSize,Size2,Cts3),
      rewrite_term_with_constraint_6(Cts3,T,N,Cts4),
      (rtwc_stop -> (
        Cts2=Cts4
      ); (
        append(Cts1,Cts4,Cts5),
        N2 is N-1,
        rewrite_term_with_constraint_5(N2,T,Sp,Ds,V,Con,TSize,Size2,Cts5,Cts2)
      )).
    rewrite_term_with_constraint_6([],_,_,[]) :- !.
    rewrite_term_with_constraint_6([[Ti,F,Con]|Cts1],T1,N,[[T2,F,Con]|Cts2]) :-
      T1=..[Func|Ts1],
      replace_list(Ts1,N,Ti,Ts2),
      T2=..[Func|Ts2],
      rewrite_term_with_constraint_6(Cts1,T1,N,Cts2).
    rewrite_term_with_constraint_7([],_,[]) :- !.
    rewrite_term_with_constraint_7([[_,_,Con1]|Cts],Con2,[Con3|Cons]) :-
      identical_set_difference(Con1,Con2,Con3),
      rewrite_term_with_constraint_7(Cts,Con2,Cons).
    rewrite_term_with_constraint_8([],_,[]) :-!.
    rewrite_term_with_constraint_8([Con1|Cons1],Con2,[Con3|Cons2]) :-
      append(Con2,Con1,Con4),
      identical_delete_all_duplicates(Con4,Con3),
      constraint_consistent(Con3),
      !,
      rewrite_term_with_constraint_8(Cons1,Con2,Cons2).
    rewrite_term_with_constraint_8([_|Cons1],Con,Cons2) :-
      rewrite_term_with_constraint_8(Cons1,Con,Cons2).
    rewrite_term_with_constraint_9([],_,[]) :- !.
    rewrite_term_with_constraint_9([Con|Cons],T,[[T,0,Con]|Cts]) :-
      rewrite_term_with_constraint_9(Cons,T,Cts).
    rewrite_term_with_constraint_10([],_,_,_,Cts,Cts) :- !.
    rewrite_term_with_constraint_10([[T,0,Con]|Cts1],Sp,Ds,V,Cts2,Cts3) :-
      !,
      rewrite_term_with_constraint_1(T,Sp,Ds,V,Con,Cts4),
      append(Cts2,Cts4,Cts5),
      rewrite_term_with_constraint_10(Cts1,Sp,Ds,V,Cts5,Cts3).
    rewrite_term_with_constraint_10([[T,1,Con]|Cts1],Sp,Ds,V,Cts2,Cts3) :-
      append(Cts2,[[T,1,Con]],Cts4),
      rewrite_term_with_constraint_10(Cts1,Sp,Ds,V,Cts4,Cts3).

%%%
%%% rewrite_term_args_only_with_constraint(T,Sp,Ds,Con,Cts)
%%%   input
%%%     T   : term
%%%     Sp  : support data for computing priority
%%%     Ds  : distance data for computing priority
%%%     Con : constraint
%%%   output
%%%     Cts : set of simplified term/flag/constraint triples obtained by
%%%           rewriting the arguments of T under the constraint C.  Flag is
%%%           set as follows:
%%%             0 -- term fully rewritten
%%%             1 -- rewrite terminated early due to priority
%%%   notes
%%%     If Sp is uninstantiated, the priority is not checked after using a
%%%       marked equational rule.
%%%
    rewrite_term_args_only_with_constraint(T,_,_,Con,[[T,0,Con]]) :-
      var(T),
      !.
    rewrite_term_args_only_with_constraint(T,Sp,Ds,Con,Cts) :-
      functor(T,F,N),
      rewrite_term_args_only_with_constraint_1(N,T,Sp,Ds,Con,Cts1),
      rewrite_term_args_only_with_constraint_4(Cts1,F,Cts).
    rewrite_term_args_only_with_constraint_1(0,_,_,_,Con,[[[],0,Con]]) :- !.
    rewrite_term_args_only_with_constraint_1(N,T,Sp,Ds,Con,Cts) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,Ti),
      rewrite_term_with_constraint(Ti,Sp,Ds,Con,Cts1),
      N3 is N-1,
      rewrite_term_args_only_with_constraint_2(Cts1,N3,T,Sp,Ds,[],Cts).
    rewrite_term_args_only_with_constraint_2([],_,_,_,_,Cts,Cts) :- !.
    rewrite_term_args_only_with_constraint_2([[Ti,0,Con]|Cts1],N,T,Sp,Ds,Cts2,
        Cts3) :-
      !,
      rewrite_term_args_only_with_constraint_1(N,T,Sp,Ds,Con,Cts4),
      rewrite_term_args_only_with_constraint_3(Cts4,Ti,Cts5),
      append(Cts2,Cts5,Cts6),
      rewrite_term_args_only_with_constraint_2(Cts1,N,T,Sp,Ds,Cts6,Cts3).
    rewrite_term_args_only_with_constraint_2([[Ti,1,Con]|Cts1],N,T,Sp,Ds,Cts2,
        Cts3) :-
      append(Cts2,[[[Ti|Ts],1,Con]],Cts4),
      rewrite_term_args_only_with_constraint_2(Cts1,N,T,Sp,Ds,Cts4,Cts3).
    rewrite_term_args_only_with_constraint_3([],_,[]) :- !.
    rewrite_term_args_only_with_constraint_3([[Ts,F,Con]|Cts1],Ti,
        [[[Ti|Ts],F,Con]|Cts2]) :-
      rewrite_term_args_only_with_constraint_3(Cts1,Ti,Cts2).
    rewrite_term_args_only_with_constraint_4([],_,[]) :- !.
    rewrite_term_args_only_with_constraint_4([[Ts,F,Con]|Cts1],Func,
        [[T,F,Con]|Cts2]) :-
      T=..[Func|Ts],
      rewrite_term_args_only_with_constraint_4(Cts1,Func,Cts2).

%%%
%%% simplify_constraint_triples(Cts1,Cts2)
%%%   input
%%%     Cts1 : set of constraint triples
%%%   output
%%%     Cts2 : Cts1 with redundant constraint triples deleted.  A constraint
%%%            triple [T1,F1,Con1] is redundant if there exist another
%%%            constraint triple [T2,F2,Con2] such that Con1 implies Con2.
%%%
    simplify_constraint_triples(Cts1,Cts2) :-
      identical_delete_all_duplicates(Cts1,Cts3),
      simplify_constraint_triples_1(Cts3,Cts3,Cts2).
    simplify_constraint_triples_1([],Cts,Cts) :- !.
    simplify_constraint_triples_1([Ct|Cts1],Cts2,Cts3) :-
      (simplify_constraint_triples_2(Ct,Cts2) -> (
        identical_delete_all(Ct,Cts2,Cts4),
        simplify_constraint_triples_1(Cts1,Cts4,Cts3)
      ); simplify_constraint_triples_1(Cts1,Cts2,Cts3)).
    simplify_constraint_triples_2([T1,F1,Con1],[[T2,F2,Con2]|Cts]) :-
      (([T1,F1,Con1]\==[T2,F2,Con2], implies_constraint(Con1,Con2)) -> true; (
        simplify_constraint_triples_2([T1,F1,Con1],Cts)
      )).

%%%
%%% implies_constraint(Con1,Con2)
%%%   input
%%%     Con1 : consistent constraint
%%%     Con2 : consistent constraint
%%%   exceptions
%%%     fails if C1 does not imply C2
    implies_constraint(Con1,Con2) :-
      identical_set_difference(Con2,Con1,Con3),
      implies_constraint_1(Con3,Con1).
    implies_constraint_1([],_) :- !.
    implies_constraint_1([S>T|Con1],Con2) :-
      not(constraint_consistent([T>S|Con2])),
      implies_constraint_1(Con1,Con2).

%%%
%%% negate_constraints(Cons1,Cons2)
%%%   input
%%%     Cons1 : set of constraints
%%%   output
%%%     Cons2 : negation of Cons2
%%%
    negate_constraints(Cons1,Cons2) :-
      bagof1(Con,negate_constraints_1(Cons1,[],Con),Cons3),
      identical_delete_all_duplicates(Cons3,Cons4),
      negate_constraints_2(Cons4,Cons4,Cons2).
    negate_constraints_1([],Con,Con).
    negate_constraints_1([Con1|Cons],Con2,Con3) :-
      member(S>T,Con1),
      append(Con2,[T>S],Con4),
      constraint_consistent(Con4),
      negate_constraints_1(Cons,Con4,Con3).
    negate_constraints_2([],Cons,Cons) :- !.
    negate_constraints_2([Con|Cons1],Cons2,Cons3) :-
      (negate_constraints_3(Con,Cons2) -> (
        identical_delete_all(Con,Cons2,Cons4),
        negate_constraints_2(Cons1,Cons4,Cons3)
      ); negate_constraints_2(Cons1,Cons2,Cons3)).
    negate_constraints_3(Con1,[Con2|Cons]) :-
      ((Con1\==Con2, implies_constraint(Con1,Con2)) -> true; (
        negate_constraints_3(Con,Cons)
      )).

%%%
%%% Constraint_consistent(Con)
%%%   input
%%%     Con : constraint
%%%   exceptions
%%%     fails if constraint is not consistent
%%%
    constraint_consistent([]) :- !.
    constraint_consistent([S>T]) :-
     !,
      order_term(S,O,T),
      ((O=='>'; O=='!') -> true; fail).
    constraint_consistent(Con) :-
      vars_tail(Con,V),
      constraint_consistent_1(Con,V).
    constraint_consistent_1(Con,V) :-
%      not(not((
%        var_list(V),
%        write('*** entered constraint_consistent_1('),
%        write(Con),
%        write(',V)'),
%        write_line(0,'')
%      ))),
      term_size(Con,Size),
      ((not(not((
          const_list(V),
          cached_constraint_consistent(Size,Con,V,F),
          assert(ccc_flag(F)))))) -> (
        retract(ccc_flag(F)),
        (F==0 -> fail; true)
      ); (
        counter(cached_constraint_consistent_count,N),
        cache_size(CacheSize),
        (N > CacheSize -> (
          write_line(0,'*** cleared cached_constraint_consistent: ',N),
          set_counter(cached_constraint_consistent_count,0),
          abolish(cached_constraint_consistent,4)
        ); true),
        increment_counter(cached_constraint_consistent_count,Size),
        (not(not(constraint_consistent_2(Con,V))) -> (
          assert(cached_constraint_consistent(Size,Con,V,1))
        ); (
          assert(cached_constraint_consistent(Size,Con,V,0)),
          fail
        ))
      )).
    constraint_consistent_2(Con,V) :-
      constraint_consistent_3(Con),
      constraint_consistent_4(Con,[],Con1),
      (Con1==[] -> true; (
        ((member_N(Con1,S>T,Con2), nonvar(S), nonvar(T)) -> (
          order_term_with_constraint(S,T,Con3),
          append(Con2,Con3,Con4),
          identical_delete_all_duplicates(Con4,Con5),
          constraint_consistent_1(Con5,V)
        ); (
          (constraint_consistent_5(Con1,X) -> (
            bagof1(Cond,constraint_consistent_8(Con1,X,Cond),Con2),
            constraint_consistent_9(Con1,X,[],Con3),
            append(Con3,Con2,Con4),
            identical_delete_all_duplicates(Con4,Con5),
            constraint_consistent_1(Con5,V)
          ); fail)
        ))
      )).
    constraint_consistent_3([]) :- !.
    constraint_consistent_3([S>T|Con]) :-
      not(identical_member(T>S,Con)),
      constraint_consistent_3(Con).
    constraint_consistent_4([],Con,Con) :- !.
    constraint_consistent_4([S>T|Con1],Con2,Con3) :-
      (is_subterm(S,T) -> fail; (
        (is_subterm(T,S) -> (
          constraint_consistent_4(Con1,Con2,Con3)
        ); (
          append(Con2,[S>T],Con4),
          constraint_consistent_4(Con1,Con4,Con3)
        ))
      )).
    constraint_consistent_5(Con,X) :-
      list_vars(Con,Vs),
      constraint_consistent_6(Vs,Con,X).
    constraint_consistent_6([V|Vs],Con,X) :-
      (constraint_consistent_7(Con,V) -> (
        X=V
      ); (
        constraint_consistent_6(Vs,Con,X)
      )).
    constraint_consistent_7([],_) :- !.
    constraint_consistent_7([_>T|Con],V) :-
      (V==T; not(identical_embedded(V,T))),
      !,
      constraint_consistent_7(Con,V).
    constraint_consistent_8(Con1,X,S3>T2) :-
      member(S1>T1,Con1),
      T1==X,
      member(S2>T2,Con1),
      identical_embedded(X,S2),
      substitute_term_all(S2,X,S1,S3).
    constraint_consistent_9([],_,Con,Con) :- !.
    constraint_consistent_9([S>T|Con1],X,Con2,Con3) :-
      ((T==X; identical_embedded(X,S)) -> (
        constraint_consistent_9(Con1,X,Con2,Con3)
      ); (
        append(Con2,[S>T],Con4),
        constraint_consistent_9(Con1,X,Con4,Con3)
      )).

%%%
%%% Order_term_with_constraint(S,T,Con)
%%%   input
%%%     S   : term
%%%     T   : term
%%%   output
%%%     Con : consistent constraint under which S > T
%%%   exceptions
%%%     fails if not S > T under any consistent constraint
%%%   notes
%%%     additional consistent constraints under which S > T are returned on
%%%       backtracking
%%%     order_term_with_constraint is only supported for lpo
%%%
    order_term_with_constraint(S,T,Con) :-
      (term_ordering(lpo) -> (
        order_term_lpo_with_constraint(S,T,Con)
      ); (
        (term_ordering(X) -> (
          write_line(5,'Invalid term ordering: ',X),
          abort
        ); (
          write_line(5,'No term ordering'),
          abort
        ))
      )).

%%%
%%% Order_term_lpo_with_constraint(S,T,Con)
%%%   input
%%%     S   : term
%%%     T   : term
%%%   output
%%%     Con : constraint consistent with respect to lpo under which S > T
%%%   exceptions
%%%     fails if not S > T under any constraint consistent with respect to lpo
%%%   notes
%%%     additional constraints consistent with respect to lpo under which
%%%       S > T are returned on backtracking
%%%
    order_term_lpo_with_constraint(S,T,Con) :-
      counter(cached_constrained_term_order_count,N),
      cache_size(CacheSize),
      (N > CacheSize -> (
        write_line(0,'*** cleared cached_constrained_term_order: ',N),
        set_counter(cached_constrained_term_order_count,0),
        abolish(cached_constrained_term_order,5),
        abolish(cached_constrained_term_order_complete,4)
      ); true),
      vars_tail({S,T},V),
      term_size_structure(S,SSize),
      term_size_structure(T,TSize),
      order_term_lpo_with_constraint_1(S,T,Con,V,SSize,TSize).
    order_term_lpo_with_constraint_1(S,T,Con,V,SSize,TSize) :-
      arg(1,SSize,Size1),
      arg(1,TSize,Size2),
      Size3 is (Size1*10000)+Size2,
      order_term_lpo_with_constraint_2(Size1,Size2,Size3,S,T,V,Con,SSize,
        TSize).
    order_term_lpo_with_constraint_2(_,_,Size3,S,T,V,Con,_,_) :-
      cached_constrained_term_order(Size3,S,T,var(V1,V2,V3),Con),
      not(not(const_list(V))),
      not(not(const_list(V3))),
      not(not((V1=V2,const_list(V)))).
    order_term_lpo_with_constraint_2(Size1,Size2,Size3,S,T,V,Con,SSize,
        TSize) :-
      not((
        const_list(V),
        cached_constrained_term_order_complete(Size3,S,T,V)
      )),
      order_term_lpo_with_constraint_3(S,T,Con,V,SSize,TSize),
      not((
        const_list(V),
        cached_constrained_term_order(Size3,S,T,var(V1,V1,V),Con)
      )),
      term_size(Con,Size4),
      linearize_term({S,T},{S1,T1},V1,V2),
      Size5 is Size1+Size2+Size4,
      increment_counter(cached_constrained_term_order_count,Size5),
      assert(cached_constrained_term_order(Size3,S1,T1,var(V1,V2,V),Con)).
    order_term_lpo_with_constraint_2(Size1,Size2,Size3,S,T,V,_,_,_) :-
      !,
      not((
        const_list(V),
        cached_constrained_term_order_complete(Size3,S,T,V)
      )),
      Size4 is Size1+Size2,
      increment_counter(cached_constrained_term_order_count,Size4),
      assert(cached_constrained_term_order_complete(Size3,S,T,V)),
      fail.
    order_term_lpo_with_constraint_3(S,T,Con,V,SSize,TSize) :-
      order_term_lpo(S,O,T),
      ((O=='<'; O=='=') -> fail; (
        (O=='>' -> (Con=[]); (
          ((var(S); var(T)) -> (Con=[S>T]); (
            (
              functor(S,_,N),
              order_term_lpo_with_constraint_4(N,S,T,Con,V,SSize,TSize)
            ); (
              functor(S,Sf,Sn),
              functor(T,Tf,Tn),
              (lex_eq(Sf,Sn,Tf,Tn) -> (
                order_term_lpo_with_constraint_5(Sn,S,T,[],Con,V,SSize,TSize)
              ); (
                (lex_gt(Sf,Sn,Tf,Tn) -> (
                  order_term_lpo_with_constraint_7(Tn,S,T,[],Con,V,SSize,TSize)
                ); fail)
              ))
            )
          ))
        ))
      )).
    order_term_lpo_with_constraint_4(N,S,T,Con,V,SSize,TSize) :-
      enumerate(1,N,1,I),
      arg(I,S,Si),
      I1 is I+1,
      arg(I1,SSize,SiSize),
      order_term_lpo_with_constraint_1(Si,T,Con,V,SiSize,TSize).
    order_term_lpo_with_constraint_5(0,_,_,_,_,_,_,_) :-
      !,
      fail.
    order_term_lpo_with_constraint_5(N,S,T,Con1,Con2,V,SSize,TSize) :-
      functor(S,_,N1),
      N2 is N1-N+1,
      arg(N2,S,Si),
      arg(N2,T,Ti),
      equal_term_lpo_with_constraint(Si,Ti,Con3),
      append(Con1,Con3,Con4),
      identical_delete_all_duplicates(Con4,Con5),
      constraint_consistent(Con5),
      N3 is N-1,
      order_term_lpo_with_constraint_5(N3,S,T,Con5,Con2,V,SSize,TSize).
    order_term_lpo_with_constraint_5(N,S,T,Con1,Con2,V,SSize,TSize) :-
      functor(S,_,N1),
      N2 is N1-N+1,
      arg(N2,S,Si),
      arg(N2,T,Ti),
      N3 is N2+1,
      arg(N3,SSize,SiSize),
      arg(N3,TSize,TiSize),
      order_term_lpo_with_constraint_1(Si,Ti,Con3,V,SiSize,TiSize),
      append(Con1,Con3,Con4),
      identical_delete_all_duplicates(Con4,Con5),
      constraint_consistent(Con5),
      N4 is N-1,
      order_term_lpo_with_constraint_6(N4,S,T,Con5,Con2,V,SSize,TSize).
    order_term_lpo_with_constraint_6(0,_,_,Con,Con,_,_,_) :- !.
    order_term_lpo_with_constraint_6(N,S,T,Con1,Con2,V,SSize,TSize) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,Ti),
      N3 is N2+1,
      arg(N3,TSize,TiSize),
      order_term_lpo_with_constraint_1(S,Ti,Con3,V,SSize,TiSize),
      append(Con1,Con3,Con4),
      identical_delete_all_duplicates(Con4,Con5),
      constraint_consistent(Con5),
      N4 is N-1,
      order_term_lpo_with_constraint_6(N4,S,T,Con5,Con2,V,SSize,TSize).
    order_term_lpo_with_constraint_7(0,_,_,Con,Con,_,_,_).
    order_term_lpo_with_constraint_7(N,S,T,Con1,Con2,V,SSize,TSize) :-
      functor(T,_,N1),
      N2 is N1-N+1,
      arg(N2,T,Ti),
      N3 is N2+1,
      arg(N3,TSize,TiSize),
      order_term_lpo_with_constraint_1(S,Ti,Con3,V,SSize,TiSize),
      append(Con1,Con3,Con4),
      identical_delete_all_duplicates(Con4,Con5),
      constraint_consistent(Con5),
      N4 is N-1,
      order_term_lpo_with_constraint_7(N4,S,T,Con5,Con2,V,SSize,TSize).

%%%
%%% Equal_term_lpo_with_constraint(S,T,Con)
%%%   input
%%%     S   : term
%%%     T   : term
%%%   output
%%%     Con : constraint consistent with respect to lpo under which S = T
%%%   exceptions
%%%     fails if not S > T under any constraint consistent with respect to lpo
%%%   notes
%%%     additional constraints consistent with respect to lpo under which
%%%       S = T are returned on backtracking
%%%
    equal_term_lpo_with_constraint(S,T,Con) :-
      order_term_lpo(S,O,T),
      ((O=='<'; O=='>') -> fail; (
        (O=='=' -> (Con=[]); (
          ((var(S); var(T)) -> (
            fail
          ); (
            functor(S,Sf,Sn),
            functor(T,Tf,Tn),
            (lex_eq(Sf,Sn,Tf,Tn) -> (
              equal_term_lpo_with_constraint_1(Sn,S,T,[],Con)
            ); fail)
          ))
        ))
      )).
    equal_term_lpo_with_constraint_1(0,_,_,Con,Con) :- !.
    equal_term_lpo_with_constraint_1(N,S,T,Con1,Con2) :-
      functor(S,_,N1),
      N2 is N1-N+1,
      arg(N2,S,Si),
      arg(N2,T,Ti),
      equal_term_lpo_with_constraint(Si,Ti,Con3),
      append(Con1,Con3,Con4),
      identical_delete_all_duplicates(Con4,Con5),
      constraint_consistent(Con5),
      N3 is N-1,
      equal_term_lpo_with_constraint_1(N3,S,T,Con5,Con2).

%%%
%%% rewrite_replace_rules
%%%
    rewrite_replace_rules :-
      bagof1([R,V,F,C],W^replace_rule_1(R,V,W,F,C),Rules_1),
      rewrite_replace_rules_1(Rules_1),
      bagof1([R,V,F,C],W^replace_rule_2(R,V,W,F,C),Rules_2),
      rewrite_replace_rules_5(Rules_2).
    rewrite_replace_rules_1([]) :- !.
    rewrite_replace_rules_1([[R,V,F,C]|Rules]) :-
      (constrained_rewriting -> (
        (restricted_rewrite -> (
          abolish(restricted_rewrite,0),
          rewrite_clause_with_constraint(R,_,_,[],Cts),
          assert(restricted_rewrite)
        ); (
          rewrite_clause_with_constraint(R,_,_,[],Cts)
        )),
        rewrite_replace_rules_2(Cts,Rs1),
        identical_delete_all_duplicates(Rs1,Rs2),
        identical_delete_all(R,Rs2,Rs3),
        (Rs2==Rs3 -> (
          not(not(rewrite_replace_rules_3(R,V)))
        ); true),
        rewrite_replace_rules_4(Rs3,F,C)
      ); (
        (restricted_rewrite -> (
          abolish(restricted_rewrite,0),
          rewrite_clause(R,_,_,0,R1,_),
          assert(restricted_rewrite)
        ); (
          rewrite_clause(R,_,_,0,R1,_)
        )),
        (R\==R1 -> (
          not(not(rewrite_replace_rules_3(R,V))),
          vars_tail(R1,V1),
          (not(duplicate_repeated_replace_rule(R1,V1)) -> (
            vars_literals(R1,W1),
            assert(replace_rule_1(R1,V1,W1,F,C))
          ); true)
        ); true)
      )),
      rewrite_replace_rules_1(Rules).
    rewrite_replace_rules_2([],[]) :- !.
    rewrite_replace_rules_2([[R,_,_]|Cts],[R|Rs]) :-
      rewrite_replace_rules_2(Cts,Rs).
    rewrite_replace_rules_3(R,V) :-
      const_list(V),
      retract(replace_rule_1(R,V,_,_,_)),
      !.
    rewrite_replace_rules_4([],_,_) :- !.
    rewrite_replace_rules_4([R|Rs],F,C) :-
      vars_tail(R,V),
      (not(duplicate_repeated_replace_rule(R,V)) -> (
        vars_literals(R,W),
        assert(replace_rule_1(R,V,W,F,C))
      ); true),
      rewrite_replace_rules_4(Rs,F,C).
    rewrite_replace_rules_5([]) :- !.
    rewrite_replace_rules_5([[R,V,F,C]|Rules]) :-
      (constrained_rewriting -> (
        (restricted_rewrite -> (
          abolish(restricted_rewrite,0),
          rewrite_clause_with_constraint(R,_,_,[],Cts),
          assert(restricted_rewrite)
        ); (
          rewrite_clause_with_constraint(R,_,_,[],Cts)
        )),
        rewrite_replace_rules_2(Cts,Rs1),
        identical_delete_all_duplicates(Rs1,Rs2),
        identical_delete_all(R,Rs2,Rs3),
        (Rs2==Rs3 -> (
          not(not(rewrite_replace_rules_6(R,V)))
        ); true),
        rewrite_replace_rules_7(Rs3,F,C)
      ); (
        (restricted_rewrite -> (
          abolish(restricted_rewrite,0),
          rewrite_clause_np(R,_,_,0,R1,_),
          assert(restricted_rewrite)
        ); (
          rewrite_clause_np(R,_,_,0,R1,_)
        )),
        (R\==R1 -> (
          not(not(rewrite_replace_rules_6(R,V))),
          vars_tail(R1,V1),
          (not(duplicate_once_replace_rule(R1,V1)) -> (
            vars_literals(R1,W1),
            assert(replace_rule_2(R1,V1,W1,F,C))
          ); true)
        ); true)
      )),
      rewrite_replace_rules_5(Rules).
    rewrite_replace_rules_6(R,V) :-
      const_list(V),
      retract(replace_rule_2(R,V,_,_,_)),
      !.
    rewrite_replace_rules_7([],_,_) :- !.
    rewrite_replace_rules_7([R|Rs],F,C) :-
      vars_tail(R,V),
      (not(duplicate_once_replace_rule(R,V)) -> (
        vars_literals(R,W),
        assert(replace_rule_2(R,V,W,F,C))
      ); true),
      rewrite_replace_rules_7(Rs,F,C).

%%%
%%% Abolish_rewrite_caches.
%%%
    abolish_rewrite_caches :-
      abolish(cached_rewrite,5),
      set_counter(cached_rewrite_count,0),
      abolish(cached_subterm_rewrite,6),
      set_counter(cached_subterm_rewrite_count,0),
      abolish(cached_restricted_clause_rewrite,4),
      abolish(cached_nonrestricted_clause_rewrite,4),
      set_counter(cached_clause_rewrite_count,0).